Data.Type.BitRecords.Structure.TypeLits

Documentation

type family PositiveInt (n :: Nat) where ...

A Positive Signed Nat

Equations

PositiveInt n = To (Signed Nat Nat) (Positive n :: Signed Nat Nat)

type family NegativeInt (n :: Nat) where ...

A Negative Signed Nat

Equations

NegativeInt n = To (Signed Nat Nat) (Negative n :: Signed Nat Nat)

type family Bits (xs :: [Nat]) where ...

A literal bit sequence. The sequence is validated, only zeros and ones are allowed.

Equations

Bits xs = To (Sequence Bit Nat) xs

class LiteralFamily a typeLitKind | a -> typeLitKind

A kind class for kinds, that are inhabited on type-level by a certain kind of literal.

a

This parameter identifies the whole family; a type level literal kind of the family is determined by that parameter. No two instances for the same family but with different type level literal kinds are allowed.

typeLitKind

This is the kind of type level literals representing the static values inhabiting this family.

Associated Types

type InRange a (typeLit :: typeLitKind) :: Bool

A predicate that is applied to a type-level-literal and is satisfied iff the given literal is in the range of valid type-level-literals of kind typeLitKind.

This is by SequenceLiteral for example.

type Pretty a (typeLit :: typeLitKind) :: PrettyType

Convert a type level representation to a PrettyType

type PrettySeperator a (typeLit :: typeLitKind) :: PrettyType

Seperator to use when rendering a list of literals of this family.

type SizeOf a (typeLit :: typeLitKind) :: Nat

Return the number of bits that the literal value will occupy

Instances

LiteralFamily Bool Bool

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Bool typeLit :: Bool

type Pretty Bool typeLit :: PrettyType

type PrettySeperator Bool typeLit :: PrettyType

type SizeOf Bool typeLit :: Nat

LiteralFamily Word8 Nat

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Word8 typeLit :: Bool

type Pretty Word8 typeLit :: PrettyType

type PrettySeperator Word8 typeLit :: PrettyType

type SizeOf Word8 typeLit :: Nat

LiteralFamily Word16 Nat

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Word16 typeLit :: Bool

type Pretty Word16 typeLit :: PrettyType

type PrettySeperator Word16 typeLit :: PrettyType

type SizeOf Word16 typeLit :: Nat

LiteralFamily Nat Nat

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Nat typeLit :: Bool

type Pretty Nat typeLit :: PrettyType

type PrettySeperator Nat typeLit :: PrettyType

type SizeOf Nat typeLit :: Nat

LiteralFamily () ()

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange () typeLit :: Bool

type Pretty () typeLit :: PrettyType

type PrettySeperator () typeLit :: PrettyType

type SizeOf () typeLit :: Nat

LiteralFamily Byte Nat

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Byte typeLit :: Bool

type Pretty Byte typeLit :: PrettyType

type PrettySeperator Byte typeLit :: PrettyType

type SizeOf Byte typeLit :: Nat

LiteralFamily Bit Nat

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Bit typeLit :: Bool

type Pretty Bit typeLit :: PrettyType

type PrettySeperator Bit typeLit :: PrettyType

type SizeOf Bit typeLit :: Nat

LiteralFamily Empty Empty

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Empty typeLit :: Bool

type Pretty Empty typeLit :: PrettyType

type PrettySeperator Empty typeLit :: PrettyType

type SizeOf Empty typeLit :: Nat

LiteralFamily s k => LiteralFamily (Maybe s :: Type) (Maybe k)

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange (Maybe s) typeLit :: Bool

type Pretty (Maybe s) typeLit :: PrettyType

type PrettySeperator (Maybe s) typeLit :: PrettyType

type SizeOf (Maybe s) typeLit :: Nat

(LiteralFamily as ak, LiteralFamily bs bk) => LiteralFamily ((as, bs) :: Type) (ak, bk)

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange (as, bs) typeLit :: Bool

type Pretty (as, bs) typeLit :: PrettyType

type PrettySeperator (as, bs) typeLit :: PrettyType

type SizeOf (as, bs) typeLit :: Nat

LiteralFamily t v => LiteralFamily (Signed t v :: Type) (Signed t v)

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange (Signed t v) typeLit :: Bool

type Pretty (Signed t v) typeLit :: PrettyType

type PrettySeperator (Signed t v) typeLit :: PrettyType

type SizeOf (Signed t v) typeLit :: Nat

LiteralFamily s k2 => LiteralFamily (Sequence s k2 :: Type) [k2]

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange (Sequence s k2) typeLit :: Bool

type Pretty (Sequence s k2) typeLit :: PrettyType

type PrettySeperator (Sequence s k2) typeLit :: PrettyType

type SizeOf (Sequence s k2) typeLit :: Nat

type family To s (x :: k) where ...

Make a valid Value by checking the parameters using InRange and return a Value

Equations

To s (x :: k) = If (InRange s x) (Value s k x) (TypeError (((Text "Cannot make a " :<>: ShowType s) :<>: Text " from: ") :<>: ShowType x))

data Value s k (x :: k) :: Type

The representation of a value belonging to a LiteralFamily

Instances

type PrettyStructure (LiteralStructure (Value s k1 x) :: Structure FixSize -> Type)

Defined in Data.Type.BitRecords.Structure

type PrettyStructure (LiteralStructure (Value s k1 x) :: Structure FixSize -> Type) = "LiteralStructure" <:> Pretty s x

type ToPretty (Value s k1 x :: Type)

Defined in Data.Type.BitRecords.Structure.TypeLits

type ToPretty (Value s k1 x :: Type) = Pretty s x

type GetStructureSize (LiteralStructure (Value s k1 x))

Defined in Data.Type.BitRecords.Structure

type GetStructureSize (LiteralStructure (Value s k1 x)) = SizeOf s x

data Empty

An empty type literal

Instances

LiteralFamily Empty Empty

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Empty typeLit :: Bool

type Pretty Empty typeLit :: PrettyType

type PrettySeperator Empty typeLit :: PrettyType

type SizeOf Empty typeLit :: Nat

type ToPretty Empty

Defined in Data.Type.BitRecords.Structure.TypeLits

type ToPretty Empty = PutStr "Empty"

type PrettySeperator Empty (typeLit :: Empty)

Defined in Data.Type.BitRecords.Structure.TypeLits

type PrettySeperator Empty (typeLit :: Empty) = PrettySpace

data Bit

A bit literal

Instances

LiteralFamily Bit Nat

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Bit typeLit :: Bool

type Pretty Bit typeLit :: PrettyType

type PrettySeperator Bit typeLit :: PrettyType

type SizeOf Bit typeLit :: Nat

type ToPretty Bit

Defined in Data.Type.BitRecords.Structure.TypeLits

type ToPretty Bit = PutStr "Bit"

type InRange Bit (n :: Nat)

Defined in Data.Type.BitRecords.Structure.TypeLits

type InRange Bit (n :: Nat) = (n == 0) || (n == 1)

type Pretty Bit (n :: Nat)

Defined in Data.Type.BitRecords.Structure.TypeLits

type Pretty Bit (n :: Nat) = PutNat n

type PrettySeperator Bit (_ :: Nat)

Defined in Data.Type.BitRecords.Structure.TypeLits

type PrettySeperator Bit (_ :: Nat) = PrettyEmpty

type SizeOf Bit (_ :: Nat)

Defined in Data.Type.BitRecords.Structure.TypeLits

type SizeOf Bit (_ :: Nat) = 1

data Byte

An unsigned byte literal

Instances

LiteralFamily Byte Nat

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange Byte typeLit :: Bool

type Pretty Byte typeLit :: PrettyType

type PrettySeperator Byte typeLit :: PrettyType

type SizeOf Byte typeLit :: Nat

type ToPretty Byte

Defined in Data.Type.BitRecords.Structure.TypeLits

type ToPretty Byte = PutStr "Byte"

type InRange Byte (n :: Nat)

Defined in Data.Type.BitRecords.Structure.TypeLits

type InRange Byte (n :: Nat) = n <=? 255

type Pretty Byte (n :: Nat)

Defined in Data.Type.BitRecords.Structure.TypeLits

type Pretty Byte (n :: Nat) = PutHex n

type PrettySeperator Byte (typeLit :: Nat)

Defined in Data.Type.BitRecords.Structure.TypeLits

type PrettySeperator Byte (typeLit :: Nat) = PrettySpace

type SizeOf Byte (_ :: Nat)

Defined in Data.Type.BitRecords.Structure.TypeLits

type SizeOf Byte (_ :: Nat) = 8

data Signed t v

A signed type literal for family t over GHC type literal v

Constructors

Positive v

Negative v

Instances

LiteralFamily t v => LiteralFamily (Signed t v :: Type) (Signed t v)

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange (Signed t v) typeLit :: Bool

type Pretty (Signed t v) typeLit :: PrettyType

type PrettySeperator (Signed t v) typeLit :: PrettyType

type SizeOf (Signed t v) typeLit :: Nat

type ToPretty (Signed t v :: Type)

Defined in Data.Type.BitRecords.Structure.TypeLits

type ToPretty (Signed t v :: Type) = ("Signed" <:> ToPretty t) <+> ToPretty v

type PrettySeperator (Signed t v :: Type) (typeLit :: Signed t v)

Defined in Data.Type.BitRecords.Structure.TypeLits

type PrettySeperator (Signed t v :: Type) (typeLit :: Signed t v) = PrettySpace

type InRange (Signed t v :: Type) (Positive x :: Signed t v)

Defined in Data.Type.BitRecords.Structure.TypeLits

type InRange (Signed t v :: Type) (Positive x :: Signed t v) = InRange t x

type InRange (Signed t v :: Type) (Negative x :: Signed t v)

Defined in Data.Type.BitRecords.Structure.TypeLits

type InRange (Signed t v :: Type) (Negative x :: Signed t v) = InRange t x

type Pretty (Signed t v :: Type) (Positive x :: Signed t v)

Defined in Data.Type.BitRecords.Structure.TypeLits

type Pretty (Signed t v :: Type) (Positive x :: Signed t v) = PutStr "+" <+> Pretty t x

type Pretty (Signed t v :: Type) (Negative x :: Signed t v)

Defined in Data.Type.BitRecords.Structure.TypeLits

type Pretty (Signed t v :: Type) (Negative x :: Signed t v) = PutStr "-" <+> Pretty t x

type SizeOf (Signed t v :: Type) (Positive x :: Signed t v)

Defined in Data.Type.BitRecords.Structure.TypeLits

type SizeOf (Signed t v :: Type) (Positive x :: Signed t v) = SizeOf t x + 1

type SizeOf (Signed t v :: Type) (Negative x :: Signed t v)

Defined in Data.Type.BitRecords.Structure.TypeLits

type SizeOf (Signed t v :: Type) (Negative x :: Signed t v) = SizeOf t x + 1

type ToPretty (Negative v :: Signed t k2)

Defined in Data.Type.BitRecords.Structure.TypeLits

type ToPretty (Negative v :: Signed t k2) = PutStr "-" <++> ToPretty v

type ToPretty (Positive v :: Signed t k2)

Defined in Data.Type.BitRecords.Structure.TypeLits

type ToPretty (Positive v :: Signed t k2) = PutStr "+" <++> ToPretty v

type SignedByte = Signed Byte Nat

A signed Byte

type SignedInteger = Signed Nat Nat

A signed Nat

data Sequence s k

A sequence of literals.

Instances

LiteralFamily s k2 => LiteralFamily (Sequence s k2 :: Type) [k2]

Defined in Data.Type.BitRecords.Structure.TypeLits

Associated Types

type InRange (Sequence s k2) typeLit :: Bool

type Pretty (Sequence s k2) typeLit :: PrettyType

type PrettySeperator (Sequence s k2) typeLit :: PrettyType

type SizeOf (Sequence s k2) typeLit :: Nat

type InRange (Sequence s k1 :: Type) (xs :: [k1])

Defined in Data.Type.BitRecords.Structure.TypeLits

type InRange (Sequence s k1 :: Type) (xs :: [k1])

type Pretty (Sequence s k1 :: Type) (bs :: [k1])

Defined in Data.Type.BitRecords.Structure.TypeLits

type Pretty (Sequence s k1 :: Type) (bs :: [k1])

type PrettySeperator (Sequence s k2 :: Type) ([] :: [k2])

Defined in Data.Type.BitRecords.Structure.TypeLits

type PrettySeperator (Sequence s k2 :: Type) ([] :: [k2]) = PrettySpace

type SizeOf (Sequence s k2 :: Type) ([] :: [k2])

Defined in Data.Type.BitRecords.Structure.TypeLits

type SizeOf (Sequence s k2 :: Type) ([] :: [k2]) = 0

type PrettySeperator (Sequence s k1 :: Type) (x ': xs :: [k1])

Defined in Data.Type.BitRecords.Structure.TypeLits

type PrettySeperator (Sequence s k1 :: Type) (x ': xs :: [k1]) = PrettyNewline

type SizeOf (Sequence s k1 :: Type) (x ': xs :: [k1])

Defined in Data.Type.BitRecords.Structure.TypeLits

type SizeOf (Sequence s k1 :: Type) (x ': xs :: [k1]) = SizeOf s x + SizeOf (Sequence s k1) xs

type ToPretty (Sequence t v :: Type)

Defined in Data.Type.BitRecords.Structure.TypeLits

type ToPretty (Sequence t v :: Type) = "Sequence of" <:> ToPretty t