{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
-- | NamedStructure definition for sequences of bits.
--
-- This module provides the core data types and functions for
-- conversion of finite bit sequences from an to conventional (Haskell) data types.
--
-- Non-compressed, non-random finite bit sequences generated by programs are
-- usually compositions of bytes and multi byte words, and a ton of Haskell libraries
-- exist for the serialization and deserialization of ByteStrings.
--
-- This module allows the definition of a __structure__ i.e. a very simple grammar,
-- which allows functions in this library to read and write single bytes, words and bits.
--
-- Also complete bit sequence may be constructed or destructed from and to Haskell types.
--
-- Further more, the structures may contain dependent sub-sequences, for example to
-- express structures that precede a /length/ field before a repetitive block data.
--
-- Antother example for dependent sequences is /fields/ whose presence depends on
-- /flags/ preceding them.
--
-- This library is also designed with /zero copying/ in mind.
--
-- It should be emphasized that binary deserialization __is not__
-- to be confused with binary destructuring. While the former usually involves copying
-- all regular sub sequences from the input to a value of a certain type, the later
-- merely requires to peek into the sequeuence at a certain position and deserializing
-- a sub sequence. The starting position and the interpretation are governed by the
-- strucuture applied to the sequence.

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
import           Data.Type.BitRecords.Builder.LazyByteStringBuilder
import Data.FunctionBuilder
import Data.Type.BitRecords.Builder.BitBuffer64
import Control.Category
import Prelude hiding ((.), id)

-- * Bit-Records

-- ** Bit-Record Type

-- data BitRec where
--   BRFields :: [(Symbol, Extends (BitRecordField t))] -> BitRec



-- | 'BitRecordField's assembly
data BitRecord where
  EmptyBitRecord     :: BitRecord
  BRMemberT          :: Symbol -> Extends (BitRecordField t) -> BitRecord
  BitRecordMember    :: Extends (BitRecordField t) -> BitRecord
  MkRecordField      :: Extends (BitField rt st size) -> BitRecord
  BitRecordAppend    :: BitRecord -> BitRecord -> BitRecord
  -- TODO  MissingBitRecord          :: ErrorMessage     -> BitRecord



-- | A conditional 'BitRecord'
type family WhenR (b :: Bool) (x :: BitRecord) :: BitRecord where
  WhenR 'False r = 'EmptyBitRecord
  WhenR 'True r  = r

-- *** Basic Accessor

-- | Get the number of bits in a 'BitRecord'
type family SizeInBits (x :: k) :: Nat where
  SizeInBits 'EmptyBitRecord           = 0
  SizeInBits ('BitRecordMember f)      = FieldWidth f
  SizeInBits ('MkRecordField f) = BitFieldSize (From f)
  SizeInBits ('BitRecordAppend l r)    = SizeInBits l + SizeInBits r


-- | For something to be augmented by a size field there must be an instance of
-- this family to generate the value of the size field, e.g. by counting the
-- elements.
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

-- | Get the total number of members in a record.
type family BitRecordMemberCount (b :: BitRecord) :: Nat where
  BitRecordMemberCount 'EmptyBitRecord           = 0
  BitRecordMemberCount ('BitRecordMember f)      = 1
  BitRecordMemberCount ('MkRecordField f) = 1
  BitRecordMemberCount ('BitRecordAppend l r)    = BitRecordMemberCount l + BitRecordMemberCount r

-- | Get the size of the record.
getRecordSizeFromProxy
  :: forall px (rec :: BitRecord)
   . KnownNat (SizeInBits rec)
  => px rec
  -> Integer
getRecordSizeFromProxy _ = natVal (Proxy :: Proxy (SizeInBits rec))

-- | Either use the value from @Just@ or return a 'EmptyBitRecord' value(types(kinds))
type OptionalRecordOf (f :: Extends (s -> Extends BitRecord)) (x :: Maybe s)
  = (Optional (Konst 'EmptyBitRecord) f $ x :: Extends BitRecord)

-- ** Record composition

-- | Combine two 'BitRecord's to form a new 'BitRecord'. If the parameters are
-- not of type 'BitRecord' they will be converted.
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

-- | Append a 'BitRecord' and a 'BitRecordField'
type (:+.) (r :: BitRecord) (f :: Extends (BitRecordField t1))
  = Append r ( 'BitRecordMember f)
infixl 6 :+.

-- | Append a 'BitRecordField' and a 'BitRecord'
type (.+:) (f :: Extends (BitRecordField t1)) (r :: BitRecord)
  = Append ( 'BitRecordMember f) r
infixr 6 .+:

-- | Append a 'BitRecordField' and a 'BitRecordField' forming a 'BitRecord' with
-- two members.
type (.+.) (l :: Extends (BitRecordField t1)) (r :: Extends (BitRecordField t2))
  = Append ( 'BitRecordMember l) ( 'BitRecordMember r)
infixr 6 .+.

-- | Set a field to either a static value or a runtime value.
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 :~


-- -- | Like ':~' but for a 'Maybe' parameter. In case of 'Just' it behaves like ':~'
-- -- in case of 'Nothing' it return an 'EmptyBitRecord'.
-- 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 :~?

-- | Like ':~' but for a 'Maybe' parameter. In case of 'Just' it behaves like ':~'
-- in case of 'Nothing' it return an 'EmptyBitRecord'.
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 :+?

-- | The field value parameter for ':~', either a static, compile time, value or
-- a dynamic, runtime value.
data FieldValue :: Symbol -> staticRep -> Type
data StaticFieldValue (label :: Symbol) :: staticRep -> Extends (FieldValue label staticRep)
data RuntimeFieldValue (label :: Symbol) :: Extends (FieldValue label staticRep)

-- *** Record Arrays and Repitition

-- | An array of records with a fixed number of elements, NOTE: this type is
-- actually not really necessary since 'ReplicateRecord' exists, but this allows
-- to have a different 'showRecord' output.
data RecArray :: BitRecord -> Nat -> Extends BitRecord

type r ^^ n = RecArray r n
infixl 5 ^^

type instance From (RecArray (r :: BitRecord) n ) = RecArrayToBitRecord r n

-- | Repeat a bit record @n@ times.
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))

-- *** Lists of Records

-- | Let type level lists also be records
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

-- *** Maybe Record

-- | Either use the value from @Just@ or return a 'EmptyBitRecord' value(types(kinds))
data OptionalRecord :: Maybe BitRecord -> Extends BitRecord
type instance From (OptionalRecord ('Just t)) = t
type instance From (OptionalRecord 'Nothing)  = 'EmptyBitRecord

-- ** Field ADT

-- | A family of bit fields.
--
-- A bit field always has a size, i.e. the number of bits it uses, as well as a
-- term level value type and a type level value type. It also has an optional
-- label, and an optional value assigned to it.
data BitRecordField :: BitField rt st len -> Type

-- | A bit record field with a number of bits
data MkField (t :: BitField rt st len) :: Extends (BitRecordField t)

-- **** Setting a Label

-- | A bit record field with a number of bits
data LabelF :: Symbol -> Extends (BitRecordField t) -> Extends (BitRecordField t)


-- | A field with a label assigned to it.
type (l :: Symbol) @: (f :: Extends
  (BitRecordField (t :: BitField rt (st :: stk) size)))
  = (LabelF l f :: Extends (BitRecordField t))
infixr 8 @:

-- | A field with a label assigned to it.
type (l :: Symbol) @:: (f :: Extends a) = Labelled l f
infixr 8 @::

-- **** Assignment

-- | A field with a value set at compile time.
data (:=) :: forall rt st size (t :: BitField rt st size) .
            Extends (BitRecordField t)
          -> st
          -> Extends (BitRecordField t)
infixl 7 :=

-- | A field with a value set at compile time.
data (:=.) :: Extends (BitField rt st size)
           -> st
           -> Extends (BitField rt st size)
infixl 7 :=.

-- | Types of this kind define the basic type of a 'BitRecordField'. Sure, this
-- could have been an open type, but really, how many actual useful field types
-- exist? Well, from a global perspective, uncountable infinite, but the focus
-- of this library is to blast out bits over the network, using usual Haskell
-- libraries, and hence, there is actually only very little reason to
-- differentiate types of record fields, other than what low-level library
-- function to apply and how to pretty print the field.
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
    -- TODO refactor this MkFieldCustom, it caused a lot of trouble!
    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 =  MkField 'MkFieldU32
type FieldU64 = MkField 'MkFieldU64
type FieldI8 = MkField 'MkFieldI8
type FieldI16 = MkField 'MkFieldI16
type FieldI32 = MkField 'MkFieldI32
type FieldI64 = MkField 'MkFieldI64

-- | A data type for 'Field' and 'MkFieldBits', that is internally a 'Word64'.
-- It carries the number of relevant bits in its type.
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

-- | A signed field value.
data SignedNat where
  PositiveNat ::Nat -> SignedNat
  NegativeNat ::Nat -> SignedNat

-- *** Composed Fields

-- | A Flag (1-bit) that is true if the type level maybe is 'Just'.
type family FlagJust (a :: Maybe (v :: Type)) :: Extends (BitRecordField 'MkFieldFlag) where
  FlagJust ('Just x) = Flag := 'True
  FlagJust 'Nothing  = Flag := 'False

-- | A Flag (1-bit) that is true if the type level maybe is 'Nothing'.
type family FlagNothing  (a :: Maybe (v :: Type)) :: Extends (BitRecordField 'MkFieldFlag) where
  FlagNothing ('Just x) = Flag := 'False
  FlagNothing 'Nothing  = Flag := 'True

-- | A 'BitRecordField' can be used as 'BitRecordMember'
data RecordField :: Extends (BitRecordField t) -> Extends BitRecord
type instance From (RecordField f) = 'BitRecordMember f

-- | Calculate the size as a number of bits from a 'BitRecordField'
type family FieldWidth (x :: Extends (BitRecordField t)) where
  FieldWidth (x :: Extends (BitRecordField (t :: BitField rt st size))) = size

-- * Field and Record PrettyType Instances

-- | Render @rec@ to a pretty, human readable form. Internally this is a wrapper
-- around 'ptShow' using 'PrettyRecord'.
showARecord
  :: forall proxy (rec :: Extends BitRecord)
   . PrettyTypeShow (PrettyRecord (From rec))
  => proxy rec
  -> String
showARecord _ = showPretty (Proxy :: Proxy (PrettyRecord (From rec)))

-- | Render @rec@ to a pretty, human readable form. Internally this is a wrapper
-- around 'ptShow' using 'PrettyRecord'.
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 ('MkRecordField 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)

-- * Binary serialization

-- *** BitFields

instance
  forall rt st s (nested :: BitField rt st s)  .
   ( HasFunctionBuilder BitBuilder (Proxy nested) )
  => HasFunctionBuilder BitBuilder (Proxy (Konst nested)) where
  type ToFunction BitBuilder (Proxy (Konst nested)) a =
    ToFunction BitBuilder (Proxy nested) a
  toFunctionBuilder _ = toFunctionBuilder (Proxy @nested)


instance
  forall rt st s (nested :: BitField rt st s) .
   ( DynamicContent BitBuilder (Proxy nested) rt )
  => DynamicContent BitBuilder (Proxy (Konst nested)) rt where
  addParameter _ = addParameter (Proxy @nested)

-- -- *** Labbeled Fields

instance
  forall nested l .
   ( HasFunctionBuilder BitBuilder (Proxy nested) )
  => HasFunctionBuilder BitBuilder (Proxy (LabelF l nested)) where
  type ToFunction BitBuilder (Proxy (LabelF l nested)) a =
    ToFunction BitBuilder (Proxy nested) a
  toFunctionBuilder _ = toFunctionBuilder (Proxy @nested)

instance ( DynamicContent BitBuilder (Proxy nested) b )
  => DynamicContent BitBuilder (Proxy (LabelF l nested)) b where
  addParameter _ = addParameter (Proxy @nested)

instance
  forall rt st s (nested :: Extends (BitField rt st s)) l .
   ( HasFunctionBuilder BitBuilder (Proxy nested) )
  => HasFunctionBuilder BitBuilder (Proxy (Labelled l nested)) where
  type ToFunction BitBuilder (Proxy (Labelled l nested)) a =
    ToFunction BitBuilder (Proxy nested) a
  toFunctionBuilder _ = toFunctionBuilder (Proxy @nested)

instance
  forall rt st s (nested :: Extends (BitField rt st s)) (l :: Symbol)  .
   ( DynamicContent BitBuilder (Proxy nested) rt )
  => DynamicContent BitBuilder (Proxy (Labelled l nested)) rt where
  addParameter _ = addParameter (Proxy @nested)

-- -- **** Bool

instance forall f . (FieldWidth f ~ 1) =>
  HasFunctionBuilder BitBuilder (Proxy (f := 'True)) where
  toFunctionBuilder _ = immediate (appendBitBuffer64 (bitBuffer64 1 1))

instance forall f . (FieldWidth f ~ 1) =>
  HasFunctionBuilder BitBuilder (Proxy (f := 'False)) where
  toFunctionBuilder _ = immediate (appendBitBuffer64 (bitBuffer64 1 0))

instance HasFunctionBuilder BitBuilder (Proxy (MkField 'MkFieldFlag)) where
  type ToFunction BitBuilder (Proxy (MkField 'MkFieldFlag)) a = Bool -> a
  toFunctionBuilder _ =
    deferred (appendBitBuffer64 . bitBuffer64 1 . (\ !t -> if t then 1 else 0))

-- -- new:

instance forall f . (BitFieldSize (From f) ~ 1) =>
  HasFunctionBuilder BitBuilder (Proxy (f :=. 'True)) where
  toFunctionBuilder _ = immediate (appendBitBuffer64 (bitBuffer64 1 1))

instance forall f . (BitFieldSize (From f) ~ 1) =>
  HasFunctionBuilder BitBuilder (Proxy (f :=. 'False)) where
  toFunctionBuilder _ = immediate (appendBitBuffer64 (bitBuffer64 1 0))

instance HasFunctionBuilder BitBuilder (Proxy 'MkFieldFlag) where
  type ToFunction BitBuilder (Proxy 'MkFieldFlag) a = Bool -> a
  toFunctionBuilder _ =
    deferred (appendBitBuffer64 . bitBuffer64 1 . (\ !t -> if t then 1 else 0))

instance DynamicContent BitBuilder (Proxy 'MkFieldFlag) Bool where
  addParameter = toFunctionBuilder

-- -- **** Bits

instance forall (s :: Nat) . (KnownBufferSize s) =>
  HasFunctionBuilder BitBuilder (Proxy (MkField ('MkFieldBits :: BitField (B s) Nat s))) where
  type ToFunction BitBuilder (Proxy (MkField ('MkFieldBits :: BitField (B s) Nat s))) a = B s -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64ProxyLength (Proxy @s) . unB)


instance forall (s :: Nat) . (KnownBufferSize s) =>
  DynamicContent BitBuilder (Proxy (MkField ('MkFieldBits :: BitField (B s) Nat s))) (B s) where
  addParameter = toFunctionBuilder

-- -- **** Naturals

instance
  HasFunctionBuilder BitBuilder (Proxy (MkField 'MkFieldU64)) where
  type ToFunction BitBuilder (Proxy (MkField 'MkFieldU64)) a = Word64 -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64 64)

instance
  DynamicContent BitBuilder (Proxy (MkField 'MkFieldU64)) Word64 where
  addParameter = toFunctionBuilder

instance
  HasFunctionBuilder BitBuilder (Proxy (MkField 'MkFieldU32)) where
  type ToFunction BitBuilder (Proxy (MkField 'MkFieldU32)) a = Word32 -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64 32 . fromIntegral)

instance
  DynamicContent BitBuilder (Proxy (MkField ('MkFieldU32:: BitField Word32 Nat 32))) Word32 where
  addParameter = toFunctionBuilder

instance
  HasFunctionBuilder BitBuilder (Proxy 'MkFieldU32) where
  type ToFunction BitBuilder (Proxy 'MkFieldU32) a = Word32 -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64 32 . fromIntegral)

instance
  DynamicContent BitBuilder (Proxy 'MkFieldU32) Word32 where
  addParameter = toFunctionBuilder

instance
  HasFunctionBuilder BitBuilder (Proxy (MkField 'MkFieldU16)) where
  type ToFunction BitBuilder (Proxy (MkField 'MkFieldU16)) a = Word16 -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64 16 . fromIntegral)

instance
  DynamicContent BitBuilder (Proxy (MkField 'MkFieldU16)) Word16 where
  addParameter = toFunctionBuilder

instance
  HasFunctionBuilder BitBuilder (Proxy (MkField 'MkFieldU8)) where
  type ToFunction BitBuilder (Proxy (MkField 'MkFieldU8)) a = Word8 -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64 8 . fromIntegral)

instance
  DynamicContent BitBuilder (Proxy (MkField 'MkFieldU8)) Word8 where
  addParameter = toFunctionBuilder

-- -- **** Signed

instance
  HasFunctionBuilder BitBuilder (Proxy (MkField 'MkFieldI64)) where
  type ToFunction BitBuilder (Proxy (MkField 'MkFieldI64)) a = Int64 -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64 64 . fromIntegral @Int64 @Word64)

instance
  DynamicContent BitBuilder (Proxy (MkField 'MkFieldI64)) Int64 where
  addParameter = toFunctionBuilder

instance
  HasFunctionBuilder BitBuilder (Proxy (MkField 'MkFieldI32)) where
  type ToFunction BitBuilder (Proxy (MkField 'MkFieldI32)) a = Int32 -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64 32 . fromIntegral . fromIntegral @Int32 @Word32)

instance
  DynamicContent BitBuilder (Proxy (MkField 'MkFieldI32)) Int32 where
  addParameter = toFunctionBuilder

instance
  HasFunctionBuilder BitBuilder (Proxy (MkField 'MkFieldI16)) where
  type ToFunction BitBuilder (Proxy (MkField 'MkFieldI16)) a = Int16 -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64 16 . fromIntegral . fromIntegral @Int16 @Word16)

instance
  DynamicContent BitBuilder (Proxy (MkField 'MkFieldI16)) Int16 where
  addParameter = toFunctionBuilder

instance
  HasFunctionBuilder BitBuilder (Proxy (MkField 'MkFieldI8)) where
  type ToFunction BitBuilder (Proxy (MkField 'MkFieldI8)) a = Int8 -> a
  toFunctionBuilder _ = deferred (appendBitBuffer64 . bitBuffer64 8 . fromIntegral . fromIntegral @Int8 @Word8)

instance
  DynamicContent BitBuilder (Proxy (MkField 'MkFieldI8)) Int8 where
  addParameter = toFunctionBuilder

-- *** Assign static values

instance
  forall
    rt
    (len :: Nat)
    (t :: BitField rt Nat len)
    (f :: Extends (BitRecordField t))
    (v :: Nat)
    .
      ( KnownNat v
      , DynamicContent BitBuilder (Proxy f) rt
      , Num rt
      )
      =>  HasFunctionBuilder BitBuilder (Proxy (f := v)) where
  toFunctionBuilder _ =
    fillParameter (addParameter (Proxy @f)) (fromIntegral (natVal (Proxy @v)))

instance forall v f x . (KnownNat v, DynamicContent BitBuilder (Proxy f) x, Num x) =>
  HasFunctionBuilder BitBuilder (Proxy (f := 'PositiveNat v)) where
  toFunctionBuilder _ =
    fillParameter (addParameter (Proxy @f)) (fromIntegral (natVal (Proxy @v)))


instance forall v f x . (KnownNat v, DynamicContent BitBuilder (Proxy f) x, Num x) =>
  HasFunctionBuilder BitBuilder (Proxy (f := 'NegativeNat v)) where
  toFunctionBuilder _ = fillParameter (addParameter (Proxy @f)) (fromIntegral (-1 * natVal (Proxy @v)))

-- new:

instance
  forall rt (len :: Nat) (f :: Extends (BitField rt Nat len)) (v :: Nat) .
  ( KnownNat v
  , DynamicContent BitBuilder (Proxy f) rt
  , Num rt)
  =>
  HasFunctionBuilder BitBuilder (Proxy (f :=. v)) where
  toFunctionBuilder _ =
    fillParameter
      (addParameter (Proxy @f))
      (fromIntegral (natVal (Proxy @v)))

-- -- instance forall v f a x . (KnownNat v, HasFunctionBuilder BitBuilder (Proxy f) a, ToFunction BitBuilder (Proxy f) a ~ (x -> a), Num x) =>
-- --   HasFunctionBuilder BitBuilder (Proxy (f := ('PositiveNat v))) a where
-- --   toFunctionBuilder _ =  fillParameter (toFunctionBuilder (Proxy @f)) (fromIntegral (natVal (Proxy @v)))
--
--
-- -- instance forall v f a x . (KnownNat v, HasFunctionBuilder BitBuilder (Proxy f) a, ToFunction BitBuilder (Proxy f) a ~ (x -> a), Num x) =>
-- --   HasFunctionBuilder BitBuilder (Proxy (f := ('NegativeNat v))) a where
-- --   toFunctionBuilder _ = fillParameter (toFunctionBuilder (Proxy @f)) (fromIntegral (-1 * (natVal (Proxy @v))))


-- ** 'BitRecord' instances

instance forall (r :: Extends BitRecord) . HasFunctionBuilder BitBuilder (Proxy (From r)) =>
  HasFunctionBuilder BitBuilder (Proxy r) where
  type ToFunction BitBuilder (Proxy r) a =
    ToFunction BitBuilder (Proxy (From r)) a
  toFunctionBuilder _ = toFunctionBuilder (Proxy @(From r))

-- *** 'BitRecordMember'

instance forall f . HasFunctionBuilder BitBuilder (Proxy f) => HasFunctionBuilder BitBuilder (Proxy ('BitRecordMember f)) where
  type ToFunction BitBuilder (Proxy ('BitRecordMember f)) a = ToFunction BitBuilder (Proxy f) a
  toFunctionBuilder _ = toFunctionBuilder (Proxy @f)

-- *** 'RecordField'


instance forall f . HasFunctionBuilder BitBuilder (Proxy f)
  => HasFunctionBuilder BitBuilder (Proxy ('MkRecordField f)) where
  type ToFunction BitBuilder (Proxy ('MkRecordField f)) a =
        ToFunction BitBuilder (Proxy f) a
  toFunctionBuilder _ = toFunctionBuilder (Proxy @f)


-- *** 'AppendedBitRecords'

instance forall l r .
  (HasFunctionBuilder BitBuilder (Proxy l), HasFunctionBuilder BitBuilder (Proxy r))
   => HasFunctionBuilder BitBuilder (Proxy ('BitRecordAppend l r)) where
  type ToFunction BitBuilder (Proxy ('BitRecordAppend l r)) a =
    ToFunction BitBuilder (Proxy l) (ToFunction BitBuilder (Proxy r) a)
  toFunctionBuilder _ = toFunctionBuilder (Proxy @l) . toFunctionBuilder (Proxy @r)

-- *** 'EmptyBitRecord' and '...Pretty'

instance HasFunctionBuilder BitBuilder (Proxy 'EmptyBitRecord) where
  toFunctionBuilder _ = id
