{-# LANGUAGE UndecidableInstances #-}
module Data.Type.BitRecords.Sized
( type Sized, type Sized8, type Sized16, Sized32, type Sized64
, type SizedField, type SizedField8, type SizedField16, type SizedField32, type SizedField64)
where
import Data.Type.BitRecords.Core
import GHC.TypeLits
import Data.Kind.Extra
import Data.Kind (type Type)
data Sized
(sf :: Extends (BitRecordField (t :: BitField (rt :: Type) Nat (size :: Nat))))
(r :: BitRecord)
:: Extends BitRecord
type instance From (Sized sf r) =
"size" @: sf := SizeInBytes r .+: r
type Sized8 t = Sized FieldU8 t
type Sized16 t = Sized FieldU16 t
type Sized32 t = Sized2 FieldU32 t
data Sized2 ::Extends (BitField rt Nat sz) -> Extends a -> Extends BitRecord
type instance From (Sized2 sizeField (r :: Extends BitRecord)) =
'RecordField ("size" @:: sizeField :=. SizeInBytes (From r)) :+: From r
type instance From (Sized2 sizeField (r :: Extends (BitField sr st sz))) =
'RecordField ("size" @:: sizeField :=. SizeInBytes (From r)) :+: 'RecordField r
type Sized64 t = Sized FieldU64 t
data SizedField
(sf :: Extends (BitRecordField (t :: BitField (rt :: Type) Nat (size :: Nat))))
(r :: Extends (BitRecordField (u :: BitField (rt' :: Type) (st' :: k0) (len0 :: Nat))))
:: Extends BitRecord
type instance From (SizedField sf r) =
"size" @: sf := SizeInBytes r .+. r
type SizedField8 t = SizedField FieldU8 t
type SizedField16 t = SizedField FieldU16 t
type SizedField32 t = Sized32 (Konst ('RecordField t))
type SizedField64 t = SizedField FieldU64 t