{-# LANGUAGE UndecidableInstances #-}
module Data.Type.BitRecords.Core where
import Data.Int
import Data.Kind ( Type )
import Data.Kind.Extra
import Data.Proxy
import Data.Type.Pretty
import Data.Word
import Data.Bits
import GHC.TypeLits
import Text.Printf
data BitRecord where
EmptyBitRecord :: BitRecord
BitRecordMember :: Extends (BitRecordField t) -> BitRecord
RecordField :: Extends (BitField rt st size) -> BitRecord
BitRecordAppend :: BitRecord -> BitRecord -> BitRecord
type family WhenR (b :: Bool) (x :: BitRecord) :: BitRecord where
WhenR 'False r = 'EmptyBitRecord
WhenR 'True r = r
type family SizeInBits (x :: k) :: Nat where
SizeInBits 'EmptyBitRecord = 0
SizeInBits ('BitRecordMember f) = FieldWidth f
SizeInBits ('RecordField f) = BitFieldSize (From f)
SizeInBits ('BitRecordAppend l r) = SizeInBits l + SizeInBits r
type family SizeInBytes (c :: k) :: Nat
type instance SizeInBytes (f := v) = SizeInBytes v
type instance SizeInBytes (LabelF l f) = SizeInBytes f
type instance SizeInBytes (MkField (t :: BitField (rt:: Type) (st::k) (size::Nat))) = SizeInBytes t
type instance SizeInBytes (b :: BitRecord) = Bits2Bytes (SizeInBits b)
type Bits2Bytes (bitSize :: Nat) =
Bits2Bytes2 (Div bitSize 8) (Mod bitSize 8)
type family Bits2Bytes2 (bitSizeDiv8 :: Nat) (bitSizeMod8 :: Nat) :: Nat where
Bits2Bytes2 bytes 0 = bytes
Bits2Bytes2 bytes n = bytes + 1
type instance SizeInBytes (f :=. v) = SizeInBytes v
type instance SizeInBytes (Labelled l f) = SizeInBytes f
type instance SizeInBytes (t :: BitField (rt:: Type) (st::k) (size::Nat)) = size
type family BitRecordMemberCount (b :: BitRecord) :: Nat where
BitRecordMemberCount 'EmptyBitRecord = 0
BitRecordMemberCount ('BitRecordMember f) = 1
BitRecordMemberCount ('RecordField f) = 1
BitRecordMemberCount ('BitRecordAppend l r) = BitRecordMemberCount l + BitRecordMemberCount r
getRecordSizeFromProxy
:: forall px (rec :: BitRecord)
. KnownNat (SizeInBits rec)
=> px rec
-> Integer
getRecordSizeFromProxy _ = natVal (Proxy :: Proxy (SizeInBits rec))
type OptionalRecordOf (f :: Extends (s -> Extends BitRecord)) (x :: Maybe s)
= (Optional (Konst 'EmptyBitRecord) f $ x :: Extends BitRecord)
data (:+^) (l :: BitRecord) (r :: Extends BitRecord) :: Extends BitRecord
infixl 3 :+^
type instance From (l :+^ r) = l `Append` From r
data (:^+) (l :: Extends BitRecord) (r :: BitRecord) :: Extends BitRecord
infixl 3 :^+
type instance From (l :^+ r) = From l `Append` r
type (:+:) (l :: BitRecord) (r :: BitRecord) = ((l `Append` r) :: BitRecord)
infixl 3 :+:
type family Append (l :: BitRecord) (r :: BitRecord) :: BitRecord where
Append l 'EmptyBitRecord = l
Append 'EmptyBitRecord r = r
Append l r = 'BitRecordAppend l r
type (:+.) (r :: BitRecord) (f :: Extends (BitRecordField t1))
= Append r ( 'BitRecordMember f)
infixl 6 :+.
type (.+:) (f :: Extends (BitRecordField t1)) (r :: BitRecord)
= Append ( 'BitRecordMember f) r
infixr 6 .+:
type (.+.) (l :: Extends (BitRecordField t1)) (r :: Extends (BitRecordField t2))
= Append ( 'BitRecordMember l) ( 'BitRecordMember r)
infixr 6 .+.
type family (:~)
(field :: Extends (BitRecordField (t :: BitField (rt :: Type) (st :: k) (len :: Nat))))
(value :: Extends (FieldValue (label :: Symbol) st))
:: Extends (BitRecordField t) where
fld :~ StaticFieldValue l v = (l @: fld) := v
fld :~ RuntimeFieldValue l = l @: fld
infixl 7 :~
type family (:~?)
(fld :: Extends (BitRecordField (t :: BitField (rt :: Type) (st :: k) (len :: Nat))))
(value :: Maybe (Extends (FieldValue (label :: Symbol) st)))
:: Extends BitRecord where
fld :~? ('Just v) = RecordField (fld :~ v)
fld :~? 'Nothing = Konst 'EmptyBitRecord
infixl 7 :~?
type family (:+?)
(fld :: Extends (BitRecordField (t :: BitField (rt :: Type) (st :: k) (len :: Nat))))
(value :: Maybe (Extends (FieldValue (label :: Symbol) st)))
:: BitRecord where
fld :+? ('Just v) = 'BitRecordMember (fld :~ v)
fld :+? 'Nothing = 'EmptyBitRecord
infixl 7 :+?
data FieldValue :: Symbol -> staticRep -> Type
data StaticFieldValue (label :: Symbol) :: staticRep -> Extends (FieldValue label staticRep)
data RuntimeFieldValue (label :: Symbol) :: Extends (FieldValue label staticRep)
data RecArray :: BitRecord -> Nat -> Extends BitRecord
type r ^^ n = RecArray r n
infixl 5 ^^
type instance From (RecArray (r :: BitRecord) n ) = RecArrayToBitRecord r n
type family RecArrayToBitRecord (r :: BitRecord) (n :: Nat) :: BitRecord where
RecArrayToBitRecord r 0 = 'EmptyBitRecord
RecArrayToBitRecord r 1 = r
RecArrayToBitRecord r n = Append r (RecArrayToBitRecord r (n - 1))
data
BitRecordOfList
(f :: Extends (foo -> BitRecord))
(xs :: [foo])
:: Extends BitRecord
type instance From (BitRecordOfList f xs) =
FoldMap BitRecordAppendFun 'EmptyBitRecord f xs
type BitRecordAppendFun = Fun1 BitRecordAppendFun_
data BitRecordAppendFun_ :: BitRecord -> Extends (BitRecord -> BitRecord)
type instance Apply (BitRecordAppendFun_ l) r = Append l r
data OptionalRecord :: Maybe BitRecord -> Extends BitRecord
type instance From (OptionalRecord ('Just t)) = t
type instance From (OptionalRecord 'Nothing) = 'EmptyBitRecord
data BitRecordField :: BitField rt st len -> Type
data MkField t :: BitRecordField t -> Type
data LabelF :: Symbol -> Extends (BitRecordField t) -> Extends (BitRecordField t)
type (l :: Symbol) @: (f :: Extends
(BitRecordField (t :: BitField rt (st :: stk) size)))
= (LabelF l f :: Extends (BitRecordField t))
infixr 8 @:
type (l :: Symbol) @:: (f :: Extends a) = Labelled l f
infixr 8 @::
data (:=) :: forall st (t :: BitField rt st size) .
Extends (BitRecordField t)
-> st
-> Extends (BitRecordField t)
infixl 7 :=
data (:=.) :: Extends (BitField rt st size)
-> st
-> Extends (BitField rt st size)
infixl 7 :=.
data BitField
(runtimeRep :: Type)
(staticRep :: k)
(bitCount :: Nat)
where
MkFieldFlag ::BitField Bool Bool 1
MkFieldBits :: (forall (n :: Nat) . BitField (B n) Nat n)
MkFieldBitsXXL :: (forall (n :: Nat) . BitField Integer Nat n)
MkFieldU8 ::BitField Word8 Nat 8
MkFieldU16 ::BitField Word16 Nat 16
MkFieldU32 ::BitField Word32 Nat 32
MkFieldU64 ::BitField Word64 Nat 64
MkFieldI8 ::BitField Int8 SignedNat 8
MkFieldI16 ::BitField Int16 SignedNat 16
MkFieldI32 ::BitField Int32 SignedNat 32
MkFieldI64 ::BitField Int64 SignedNat 64
MkFieldCustom ::BitField rt st n
type family BitFieldSize (b :: BitField rt st size) :: Nat where
BitFieldSize (b :: BitField rt st size) = size
type Flag = MkField 'MkFieldFlag
type Field n = MkField ( 'MkFieldBits :: BitField (B n) Nat n)
type FieldU8 = MkField 'MkFieldU8
type FieldU16 = MkField 'MkFieldU16
type FieldU32 = Konst 'MkFieldU32
type FieldU64 = MkField 'MkFieldU64
type FieldI8 = MkField 'MkFieldI8
type FieldI16 = MkField 'MkFieldI16
type FieldI32 = MkField 'MkFieldI32
type FieldI64 = MkField 'MkFieldI64
newtype B (size :: Nat) = B {unB :: Word64}
deriving (Read,Show,Num,Integral,Bits,FiniteBits,Eq,Ord,Bounded,Enum,Real)
instance (PrintfArg Word64, n <= 64) => PrintfArg (B n) where
formatArg (B x) = formatArg x
parseFormat (B x) = parseFormat x
data SignedNat where
PositiveNat ::Nat -> SignedNat
NegativeNat ::Nat -> SignedNat
type family FlagJust (a :: Maybe (v :: Type)) :: Extends (BitRecordField 'MkFieldFlag) where
FlagJust ('Just x) = Flag := 'True
FlagJust 'Nothing = Flag := 'False
type family FlagNothing (a :: Maybe (v :: Type)) :: Extends (BitRecordField 'MkFieldFlag) where
FlagNothing ('Just x) = Flag := 'False
FlagNothing 'Nothing = Flag := 'True
data MaybeField :: Maybe (Extends (BitRecordField t)) -> Extends BitRecord
type instance From (MaybeField ('Just fld)) = 'BitRecordMember fld
type instance From (MaybeField 'Nothing) = 'EmptyBitRecord
data RecordField :: Extends (BitRecordField t) -> Extends BitRecord
type instance From (RecordField f) = 'BitRecordMember f
type family FieldWidth (x :: Extends (BitRecordField t)) where
FieldWidth (x :: Extends (BitRecordField (t :: BitField rt st size))) = size
showARecord
:: forall proxy (rec :: Extends BitRecord)
. PrettyTypeShow (PrettyRecord (From rec))
=> proxy rec
-> String
showARecord _ = showPretty (Proxy :: Proxy (PrettyRecord (From rec)))
showRecord
:: forall proxy (rec :: BitRecord)
. PrettyTypeShow (PrettyRecord rec)
=> proxy rec
-> String
showRecord _ = showPretty (Proxy :: Proxy (PrettyRecord rec))
type instance ToPretty (rec :: BitRecord) = PrettyRecord rec
type family PrettyRecord (rec :: BitRecord) :: PrettyType where
PrettyRecord ('BitRecordMember m) = PrettyField m
PrettyRecord ('RecordField m) = PrettyRecordField m
PrettyRecord ' EmptyBitRecord = 'PrettyNewline
PrettyRecord ('BitRecordAppend l r) = PrettyRecord l <$$> PrettyRecord r
type instance ToPretty (f :: Extends (BitRecordField t)) = PrettyField f
type family PrettyRecordField (f :: Extends (BitField (rt :: Type) (st :: Type) (size :: Nat))) :: PrettyType where
PrettyRecordField (Konst t) = PrettyFieldType t
PrettyRecordField (f :=. v) =
PrettyRecordField f <+> PutStr ":=" <+> PrettyFieldValue (From f) v
PrettyRecordField (Labelled l f) = l <:> PrettyRecordField f
type family PrettyField (f :: Extends (BitRecordField (t :: BitField (rt :: Type) (st :: Type) (size :: Nat)))) :: PrettyType where
PrettyField (MkField t) = PrettyFieldType t
PrettyField ((f :: Extends (BitRecordField t)) := v) =
PrettyField f <+> PutStr ":=" <+> PrettyFieldValue t v
PrettyField (LabelF l f) = l <:> PrettyField f
type family PrettyFieldType (t :: BitField (rt :: Type) (st :: Type) (size :: Nat)) :: PrettyType where
PrettyFieldType ('MkFieldFlag) = PutStr "boolean"
PrettyFieldType ('MkFieldBits :: BitField (B (s :: Nat)) Nat s) = PutStr "bits" <++> PrettyParens (PutNat s)
PrettyFieldType ('MkFieldBitsXXL :: BitField Integer Nat (s :: Nat)) = PutStr "bits-XXL" <++> PrettyParens (PutNat s)
PrettyFieldType ('MkFieldU64) = PutStr "U64"
PrettyFieldType ('MkFieldU32) = PutStr "U32"
PrettyFieldType ('MkFieldU16) = PutStr "U16"
PrettyFieldType ('MkFieldU8) = PutStr "U8"
PrettyFieldType ('MkFieldI64) = PutStr "I64"
PrettyFieldType ('MkFieldI32) = PutStr "I32"
PrettyFieldType ('MkFieldI16) = PutStr "I16"
PrettyFieldType ('MkFieldI8) = PutStr "I8"
PrettyFieldType ('MkFieldCustom :: BitField rt ct size) = ToPretty rt <++> PrettyParens (PutNat size)
type family PrettyFieldValue (t :: BitField (rt :: Type) (st :: Type) (size :: Nat)) (v :: st) :: PrettyType where
PrettyFieldValue ('MkFieldFlag) 'True = PutStr "yes"
PrettyFieldValue ('MkFieldFlag) 'False = PutStr "no"
PrettyFieldValue ('MkFieldBits :: BitField (B (s :: Nat)) Nat s) v =
'PrettyNat 'PrettyUnpadded ('PrettyPrecision s) 'PrettyBit v <+> PrettyParens (("hex" <:> PutHex v) <+> ("dec" <:> PutNat v))
PrettyFieldValue ('MkFieldU8) v = ("hex" <:> PutHex8 v) <+> PrettyParens ("dec" <:> PutNat v)
PrettyFieldValue ('MkFieldU16) v = ("hex" <:> PutHex16 v) <+> PrettyParens ("dec" <:> PutNat v)
PrettyFieldValue ('MkFieldU32) v = ("hex" <:> PutHex32 v) <+> PrettyParens ("dec" <:> PutNat v)
PrettyFieldValue ('MkFieldU64) v = ("hex" <:> PutHex64 v) <+> PrettyParens ("dec" <:> PutNat v)
PrettyFieldValue ('MkFieldI8) ('PositiveNat v) = ("hex" <:> (PutStr "+" <++> PutHex8 v)) <+> PrettyParens ("dec" <:> (PutStr "+" <++> PutNat v))
PrettyFieldValue ('MkFieldI16) ('PositiveNat v) = ("hex" <:> (PutStr "+" <++> PutHex16 v)) <+> PrettyParens ("dec" <:> (PutStr "+" <++> PutNat v))
PrettyFieldValue ('MkFieldI32) ('PositiveNat v) = ("hex" <:> (PutStr "+" <++> PutHex32 v)) <+> PrettyParens ("dec" <:> (PutStr "+" <++> PutNat v))
PrettyFieldValue ('MkFieldI64) ('PositiveNat v) = ("hex" <:> (PutStr "+" <++> PutHex64 v)) <+> PrettyParens ("dec" <:> (PutStr "+" <++> PutNat v))
PrettyFieldValue ('MkFieldI8) ('NegativeNat v) = ("hex" <:> (PutStr "-" <++> PutHex8 v)) <+> PrettyParens ("dec" <:> (PutStr "-" <++> PutNat v))
PrettyFieldValue ('MkFieldI16) ('NegativeNat v) = ("hex" <:> (PutStr "-" <++> PutHex16 v)) <+> PrettyParens ("dec" <:> (PutStr "-" <++> PutNat v))
PrettyFieldValue ('MkFieldI32) ('NegativeNat v) = ("hex" <:> (PutStr "-" <++> PutHex32 v)) <+> PrettyParens ("dec" <:> (PutStr "-" <++> PutNat v))
PrettyFieldValue ('MkFieldI64) ('NegativeNat v) = ("hex" <:> (PutStr "-" <++> PutHex64 v)) <+> PrettyParens ("dec" <:> (PutStr "-" <++> PutNat v))
PrettyFieldValue ('MkFieldCustom :: BitField rt ct size) v = PrettyCustomFieldValue rt ct size v
type family PrettyCustomFieldValue (rt :: Type) (st :: Type) (size :: Nat) (v :: st) :: PrettyType
type family PrintHexIfPossible t (s :: Nat) :: PrettyType where
PrintHexIfPossible Word64 s = PutHex64 s
PrintHexIfPossible Word32 s = PutHex32 s
PrintHexIfPossible Word16 s = PutHex16 s
PrintHexIfPossible Word8 s = PutHex8 s
PrintHexIfPossible x s = TypeError ('Text "Invalid size field type: " ':<>: 'ShowType x)