Ivory.BitData

quasiquoter

bitdata :: QuasiQuoter

Quasiquoter for defining Ivory bit value and bit data types.

Only the declaration and expression forms are implemented.

bit types

data Bits n

A wrapper for an Ivory type that can hold an n bit unsigned integer.

Instances

IvoryRep (BitRep n) => IvoryEq (Bits n)

IvoryRep (BitRep n) => IvoryType (Bits n)

IvoryRep (BitRep n) => IvoryVar (Bits n)

IvoryRep (BitRep n) => IvoryExpr (Bits n)

(SingI Nat n, IvoryRep (BitRep n)) => BitData (Bits n)

Identity instance of BitData for the base Bits n type.

type Bit = Bits 1

Bit is a type alias for Bits 1.

data BitArray n a

An array of n bit data elements of type a.

Instances

(SingI Nat n, SingI Nat (ArraySize n a), BitData a, IvoryRep (BitRep (ArraySize n a))) => BitData (BitArray n a)

type family BitRep n :: *

Type function: BitRep (n :: Nat) returns an Ivory type given a bit size as a type-level natural. Instances of this type family for bits [1..64] are generated using Template Haskell.

repToBits :: forall n. (SingI n, IvoryRep (BitRep n)) => BitRep n -> Bits n

Convert an Ivory value to a bit value. If the input value contains out of range bits, they will be ignored.

bitsToRep :: Bits n -> BitRep n

Convert a bit value to an Ivory value.

zeroBits :: IvoryRep (BitRep n) => Bits n

Return a bit value of all zeros of the given size.

bitLength :: forall a n. SingI n => BitArray n a -> Int

Return the number of elements in a BitArray.

bitIx :: forall a n. (BitData a, SingI n, SingI (BitSize a), SingI (ArraySize n a)) => Int -> BitDataField (BitArray n a) a

Return a BitDataField that accesses the nth element of a BitArray. This can be composed with other field accessors using .

bit data

class (SingI (BitSize (BitType a)), IvoryRep (BitDataRep a), BitType a ~ Bits (BitSize (BitType a))) => BitData a where

Class of bit data types defined by the bitdata quasiquoter.

Methods

toBits :: a -> BitType a

Convert a bit data type to its raw bit value. This is always well defined and should be exported.

fromBits :: BitType a -> a

Convert a raw bit value to a bit data type. All values may not be well defined with respect to the original set of bit data constructors. For now, we allow these junk values to be created, but that may change in the future (perhaps by implementing a checked, Ivory run-time conversion).

Instances

(SingI Nat n, IvoryRep (BitRep n)) => BitData (Bits n)

Identity instance of BitData for the base Bits n type.

(SingI Nat n, SingI Nat (ArraySize n a), BitData a, IvoryRep (BitRep (ArraySize n a))) => BitData (BitArray n a)

data BitDataField a b

Description of a bit field defined by the bitdata quasiquoter. Each field defined in the record syntax will generate a top-level definition of BitDataField.

This constructor must remain unexported so that only fields checked by the quasiquoter are created.

Instances

Show (BitDataField a b)

type BitDataRep a = BitRep (BitSize (BitType a))

The Ivory type that stores the actual value for a bit data type.

This is a shorthand to simplify the constraints on functions that take arguments of the BitData class.

bit data conversions

toRep :: BitData a => a -> BitDataRep a

Convert a bit data value to its Ivory representation.

fromRep :: BitData a => BitDataRep a -> a

Convert a raw Ivory type to a bit data type. If the input value is too large, the out of range upper bits will be masked off.

bit data field operations

setBitDataBit :: BitData a => BitDataField a Bit -> a -> a

Set a single-bit field in a bit data value.

clearBitDataBit :: BitData a => BitDataField a Bit -> a -> a

Clear a single-bit field in a bit data value.

getBitDataField :: (BitData a, BitData b, BitCast (BitDataRep a) (BitDataRep b)) => BitDataField a b -> a -> b

Extract a field from a bit data definition. Returns the value as the type defined on the right hand side of the field definition in the bitdata quasiquoter.

setBitDataField :: (BitData a, BitData b, SafeCast (BitDataRep b) (BitDataRep a)) => BitDataField a b -> a -> b -> a

Set a field from a bit data definition.

bit data operators

(#!) :: forall a n. (BitData a, SingI n, SingI (BitSize a), SingI (ArraySize n a), BitCast (BitRep (ArraySize n a)) (BitDataRep a), IvoryRep (BitRep (ArraySize n a))) => BitArray n a -> Int -> a

Return the nth element of a BitArray.

(#.) :: (BitData a, BitData b, BitCast (BitDataRep a) (BitDataRep b)) => a -> BitDataField a b -> b

Infix operator to read a bit data field. (like Data.Lens.^.)

(#>) :: BitDataField a b -> BitDataField b c -> BitDataField a c

Bit data field composition. (like Control.Category.>>>)

bit actions

data BitDataM d a

An action that modifies a bit data value of type d and returns a a in the Ivory s r monad. Values of this type are passed as the body argument to withBits etc.

Instances

Monad (BitDataM d)

Functor (BitDataM d)

runBits :: BitData d => BitDataRep d -> BitDataM d a -> (a, BitDataRep d)

Execute a bitdata action given an initial value, returning the new bitdata value and the result of the action.

withBits :: BitData d => BitDataRep d -> BitDataM d () -> BitDataRep d

Execute a bitdata action given an initial value, returning the new bitdata value.

withBitsRef :: BitData d => Ref s1 (Stored (BitDataRep d)) -> BitDataM d a -> Ivory eff a

Execute a bit data action given a reference to a value, writing the resulting value back to the reference upon completion and returning the result of the action.

clear :: BitData d => BitDataM d ()

Clear the value of the current bit data value.

setBit :: BitData d => BitDataField d Bit -> BitDataM d ()

Set a single bit field in the current bit data value.

clearBit :: BitData d => BitDataField d Bit -> BitDataM d ()

Clear a single bit.

setField :: (BitData d, BitData b, SafeCast (BitDataRep b) (BitDataRep d)) => BitDataField d b -> b -> BitDataM d ()

Set a field to a value.

bitToBool :: Bit -> IBool

Convert a single bit bitdata to an Ivory boolean.

boolToBit :: IBool -> Bit

Convert an Ivory boolean to a single bit.