{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

{-|
Module      : Polytropos.CBOR
Description : High-performance binary CBOR serialization for Polytropos records and variants
Copyright   : (c) 2026 The Polytropos Authors
License     : EUPL-1.2 OR Apache-2.0
Maintainer  : nadia.yvette.chambers@ik.me
Stability   : experimental
Portability : non-portable (GHC extensions)

High-performance binary CBOR serialization of heterogeneous and homogeneous
@polytropos@ open records and variants via @cborg@ \/ @serialise@, without intermediate
tree boxing.

= Architectural Overview & Rationale

== Binary Wire Format

* A record encodes as a standard CBOR array: one length header (the row's arity)
  followed by the flat payload field encodings in row order.
* A variant encodes as a CBOR array consisting of the constructor's 'Word' tag followed
  by that constructor's payload field encodings.

== Positional & Allocation-Free

Because field names exist only at the type level in row polymorphism, the binary
encoder is purely /positional/: no string keys are written to the wire. Encoding
and decoding are executed as single unrolled passes directly over the flat
@Rep@ payload array with no intermediate allocations.

== Truly Heterogeneous Row Support

Unlike satellites restricted to homogeneous types, @polytropos-cbor@ provides genuine
heterogeneous serialization across open rows via 'AllSerialise': every field requires
'Serialise' at /its own concrete type/, so rows mixing 'String', 'Int', 'Word', custom
types, or nested rows serialize and deserialize directly.

= When to Use This Module

* When network bandwidth, binary storage size, and serialization speed are critical.
* For inter-service RPC, binary logs, and compact caching.

= Worked Example

> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeApplications #-}
> {-# OPTIONS_GHC -fplugin=Polytropos.Plugin #-}
>
> import Codec.Serialise (serialise, deserialise)
> import Polytropos
> import Polytropos.CBOR
>
> -- A genuinely heterogeneous record:
> type Packet = Record '["id" ':= Int, "payload" ':= String, "flags" ':= Word]
>
> pkt :: Packet
> pkt = REC { id = 101, payload = "sensor-ok", flags = 0 }
>
> -- Serializes to compact positional CBOR binary:
> bytes = serialise pkt
>
> -- Deserializes back to Packet:
> pkt' :: Packet
> pkt' = deserialise bytes
-}
module Polytropos.CBOR
  ( -- * Heterogeneous Row Codecs
    AllSerialise (..)
  , FieldCount (..)
  , AllCtorsSerialise (..)

    -- * Homogeneity Evidence and Introspection Helpers
    -- $homogeneity
  , AllFieldsAre
  , AllCtorsHom (..)
  , RowField
  , SumField
  ) where

import Data.Functor.Identity (Identity (..))
import Data.Kind             (Constraint, Type)
import Data.Proxy            (Proxy (..))
import Data.Void             (Void)
import GHC.Exts              (Any, toList)
import GHC.TypeLits          (KnownSymbol, symbolVal)
import Codec.CBOR.Decoding   (Decoder, decodeListLen, decodeWord)
import Codec.CBOR.Encoding   (Encoding, encodeListLen, encodeWord)
import Codec.Serialise       (Serialise (..))
import Polytropos            (Record, Variant)
import Polytropos.Core       (Pair (..), Row, SumRow, RowRep (..), noInlineUnsafeCo,
                              productRep, injectRep, repTag, repVals)

{-------------------------------------------------------------------------------
  Heterogeneous row constraint walks
-------------------------------------------------------------------------------}

-- | Computes the arity (field count) of a row at compile time.
class FieldCount (r :: Row) where
  fieldCount :: Proxy r -> Int

instance FieldCount '[] where
  fieldCount :: Proxy '[] -> Int
fieldCount Proxy '[]
_ = Int
0

instance FieldCount r => FieldCount ((n ':= a) ': r) where
  fieldCount :: Proxy ((n ':= a) : r) -> Int
fieldCount Proxy ((n ':= a) : r)
_ = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Proxy r -> Int
forall (r :: Row). FieldCount r => Proxy r -> Int
fieldCount (forall (t :: Row). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r)

-- | Evidence that every field of the row @r@ has a 'Serialise' instance
-- at that field's own type. Serializes the erased payload slots in row order.
class AllSerialise (r :: Row) where
  encRecordCBOR :: Proxy r -> [Identity Any] -> Encoding
  decRecordCBOR :: forall s. Proxy r -> Decoder s [Identity Any]

instance AllSerialise '[] where
  encRecordCBOR :: Proxy '[] -> [Identity Any] -> Encoding
encRecordCBOR Proxy '[]
_ [Identity Any]
_ = Encoding
forall a. Monoid a => a
mempty
  decRecordCBOR :: forall s. Proxy '[] -> Decoder s [Identity Any]
decRecordCBOR Proxy '[]
_ = [Identity Any] -> Decoder s [Identity Any]
forall a. a -> Decoder s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

instance (Serialise a, AllSerialise r) => AllSerialise ((n ':= a) ': r) where
  encRecordCBOR :: Proxy ((n ':= a) : r) -> [Identity Any] -> Encoding
encRecordCBOR Proxy ((n ':= a) : r)
_ (Identity Any
x : [Identity Any]
xs) =
    a -> Encoding
forall a. Serialise a => a -> Encoding
encode (Any -> a
forall a b. a -> b
noInlineUnsafeCo Any
x :: a) Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Proxy r -> [Identity Any] -> Encoding
forall (r :: Row).
AllSerialise r =>
Proxy r -> [Identity Any] -> Encoding
encRecordCBOR (forall (t :: Row). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) [Identity Any]
xs
  encRecordCBOR Proxy ((n ':= a) : r)
_ [] = [Char] -> Encoding
forall a. HasCallStack => [Char] -> a
error [Char]
"polytropos-cbor: payload arity mismatch"

  decRecordCBOR :: forall s. Proxy ((n ':= a) : r) -> Decoder s [Identity Any]
decRecordCBOR Proxy ((n ':= a) : r)
_ = do
    x <- Decoder s a
forall s. Decoder s a
forall a s. Serialise a => Decoder s a
decode
    xs <- decRecordCBOR (Proxy @r)
    pure (Identity (noInlineUnsafeCo (x :: a) :: Any) : xs)

-- | Evidence that every constructor of the sum row @s@ has a heterogeneous
-- field row satisfying 'AllSerialise', paired with its constructor tag index.
class AllCtorsSerialise (s :: SumRow) where
  encVariantCBOR :: Proxy s -> Word -> Word -> [Identity Any] -> Encoding
  decVariantCBOR :: forall t. Proxy s -> Word -> Int -> Decoder t [Identity Any]

instance AllCtorsSerialise '[] where
  encVariantCBOR :: Proxy '[] -> Word -> Word -> [Identity Any] -> Encoding
encVariantCBOR Proxy '[]
_ Word
_ Word
_ [Identity Any]
_ = [Char] -> Encoding
forall a. HasCallStack => [Char] -> a
error [Char]
"polytropos-cbor: empty variant has no constructors"
  decVariantCBOR :: forall t. Proxy '[] -> Word -> Int -> Decoder t [Identity Any]
decVariantCBOR Proxy '[]
_ Word
_ Int
_ = [Char] -> Decoder t [Identity Any]
forall a. HasCallStack => [Char] -> Decoder t a
forall (m :: * -> *) a.
(MonadFail m, HasCallStack) =>
[Char] -> m a
fail [Char]
"polytropos-cbor: unknown constructor tag"

instance (FieldCount fs, AllSerialise fs, AllCtorsSerialise s)
      => AllCtorsSerialise ((c ':= fs) ': s) where
  encVariantCBOR :: Proxy ((c ':= fs) : s)
-> Word -> Word -> [Identity Any] -> Encoding
encVariantCBOR Proxy ((c ':= fs) : s)
_ Word
0 Word
origTag [Identity Any]
slots =
    Word -> Encoding
encodeListLen (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Proxy fs -> Int
forall (r :: Row). FieldCount r => Proxy r -> Int
fieldCount (forall (t :: Row). Proxy t
forall {k} (t :: k). Proxy t
Proxy @fs)))
      Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Word -> Encoding
encodeWord Word
origTag
      Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Proxy fs -> [Identity Any] -> Encoding
forall (r :: Row).
AllSerialise r =>
Proxy r -> [Identity Any] -> Encoding
encRecordCBOR (forall (t :: Row). Proxy t
forall {k} (t :: k). Proxy t
Proxy @fs) [Identity Any]
slots
  encVariantCBOR Proxy ((c ':= fs) : s)
_ Word
tag Word
origTag [Identity Any]
slots =
    Proxy s -> Word -> Word -> [Identity Any] -> Encoding
forall (s :: SumRow).
AllCtorsSerialise s =>
Proxy s -> Word -> Word -> [Identity Any] -> Encoding
encVariantCBOR (forall (t :: SumRow). Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) (Word
tag Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Word
origTag [Identity Any]
slots

  decVariantCBOR :: forall t.
Proxy ((c ':= fs) : s) -> Word -> Int -> Decoder t [Identity Any]
decVariantCBOR Proxy ((c ':= fs) : s)
_ Word
0 Int
len
    | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Proxy fs -> Int
forall (r :: Row). FieldCount r => Proxy r -> Int
fieldCount (forall (t :: Row). Proxy t
forall {k} (t :: k). Proxy t
Proxy @fs) = [Char] -> Decoder t [Identity Any]
forall a. HasCallStack => [Char] -> Decoder t a
forall (m :: * -> *) a.
(MonadFail m, HasCallStack) =>
[Char] -> m a
fail [Char]
"polytropos-cbor: variant field count mismatch"
    | Bool
otherwise = Proxy fs -> Decoder t [Identity Any]
forall (r :: Row) s.
AllSerialise r =>
Proxy r -> Decoder s [Identity Any]
forall s. Proxy fs -> Decoder s [Identity Any]
decRecordCBOR (forall (t :: Row). Proxy t
forall {k} (t :: k). Proxy t
Proxy @fs)
  decVariantCBOR Proxy ((c ':= fs) : s)
_ Word
tag Int
len =
    Proxy s -> Word -> Int -> Decoder t [Identity Any]
forall (s :: SumRow) t.
AllCtorsSerialise s =>
Proxy s -> Word -> Int -> Decoder t [Identity Any]
forall t. Proxy s -> Word -> Int -> Decoder t [Identity Any]
decVariantCBOR (forall (t :: SumRow). Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) (Word
tag Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) Int
len

{-------------------------------------------------------------------------------
  Record codecs
-------------------------------------------------------------------------------}

instance (FieldCount r, AllSerialise r) => Serialise (Record r) where
  encode :: Record r -> Encoding
encode (RowRep Rep Identity ()
rep) =
    Word -> Encoding
encodeListLen (Int -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy r -> Int
forall (r :: Row). FieldCount r => Proxy r -> Int
fieldCount (forall (t :: Row). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r)))
      Encoding -> Encoding -> Encoding
forall a. Semigroup a => a -> a -> a
<> Proxy r -> [Identity Any] -> Encoding
forall (r :: Row).
AllSerialise r =>
Proxy r -> [Identity Any] -> Encoding
encRecordCBOR (forall (t :: Row). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) (SmallArray (Identity Any) -> [Item (SmallArray (Identity Any))]
forall l. IsList l => l -> [Item l]
toList (Rep Identity () -> SmallArray (Identity Any)
forall {k} (f :: * -> *) (a :: k). Rep f a -> SmallArray (f Any)
repVals Rep Identity ()
rep))

  decode :: forall s. Decoder s (Record r)
decode = do
    n <- Decoder s Int
forall s. Decoder s Int
decodeListLen
    if n /= fieldCount (Proxy @r)
      then fail "polytropos-cbor: record arity mismatch"
      else do
        slots <- decRecordCBOR (Proxy @r)
        pure (RowRep (productRep slots))

{-------------------------------------------------------------------------------
  Variant codecs
-------------------------------------------------------------------------------}

instance AllCtorsSerialise s => Serialise (Variant s) where
  encode :: Variant s -> Encoding
encode (RowRep Rep Identity ()
rep) =
    let tag :: Word
tag = Rep Identity () -> Word
forall {k} (f :: * -> *) (a :: k). Rep f a -> Word
repTag Rep Identity ()
rep
    in Proxy s -> Word -> Word -> [Identity Any] -> Encoding
forall (s :: SumRow).
AllCtorsSerialise s =>
Proxy s -> Word -> Word -> [Identity Any] -> Encoding
encVariantCBOR (forall (t :: SumRow). Proxy t
forall {k} (t :: k). Proxy t
Proxy @s) Word
tag Word
tag (SmallArray (Identity Any) -> [Item (SmallArray (Identity Any))]
forall l. IsList l => l -> [Item l]
toList (Rep Identity () -> SmallArray (Identity Any)
forall {k} (f :: * -> *) (a :: k). Rep f a -> SmallArray (f Any)
repVals Rep Identity ()
rep))

  decode :: forall s. Decoder s (Variant s)
decode = do
    n <- Decoder s Int
forall s. Decoder s Int
decodeListLen
    if n < 1
      then fail "polytropos-cbor: variant encoding missing constructor tag"
      else do
        tag <- decodeWord
        slots <- decVariantCBOR (Proxy @s) tag n
        pure (RowRep (injectRep tag slots))

{-------------------------------------------------------------------------------
  Homogeneity evidence and row introspection (Reflection helpers)
-------------------------------------------------------------------------------}

-- $homogeneity
--
-- === Homogeneity Evidence and Introspection Helpers
--
-- In addition to the primary heterogeneous codecs ('AllSerialise', 'AllCtorsSerialise'),
-- this module provides closed type families and reflection classes for
-- inspecting row metadata and enforcing uniform payload types.

-- | Evidence that every field of the row @r@ has type @a@.
type family AllFieldsAre (a :: Type) (r :: Row) :: Constraint where
  AllFieldsAre _  '[]                = ()
  AllFieldsAre a ((n ':= a) ': rest) = AllFieldsAre a rest

-- | The field type of a homogeneous row: the type of every field, 'Void'
-- for the empty row.
type family RowField (r :: Row) :: Type where
  RowField '[]                 = Void
  RowField ((n ':= a) ': rest) = a

-- | The field type shared by every constructor of a sum row, 'Void' for the
-- empty sum.
type family SumField (s :: SumRow) :: Type where
  SumField '[]                = Void
  SumField ((c ':= fs) ': s)  = RowField fs

-- | Every constructor of the sum row @s@ has a homogeneous field row of type
-- @a@, reified as constructor names paired with their arities.
class AllCtorsHom (a :: Type) (s :: SumRow) where
  ctorArities :: Proxy a -> Proxy s -> [(String, Int)]

instance AllCtorsHom a '[] where
  ctorArities :: Proxy a -> Proxy '[] -> [([Char], Int)]
ctorArities Proxy a
_ Proxy '[]
_ = []

instance (KnownSymbol c, AllFieldsAre a fs, AllCtorsHom a s)
      => AllCtorsHom a ((c ':= fs) ': s) where
  ctorArities :: Proxy a -> Proxy ((c ':= fs) : s) -> [([Char], Int)]
ctorArities Proxy a
pa Proxy ((c ':= fs) : s)
_ =
    (Proxy c -> [Char]
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @c), [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Proxy fs -> [a]
arityList (forall (t :: Row). Proxy t
forall {k} (t :: k). Proxy t
Proxy @fs)))
      ([Char], Int) -> [([Char], Int)] -> [([Char], Int)]
forall a. a -> [a] -> [a]
: Proxy a -> Proxy s -> [([Char], Int)]
forall a (s :: SumRow).
AllCtorsHom a s =>
Proxy a -> Proxy s -> [([Char], Int)]
ctorArities Proxy a
pa (forall (t :: SumRow). Proxy t
forall {k} (t :: k). Proxy t
Proxy @s)
    where
      arityList :: Proxy fs -> [a]
      arityList :: Proxy fs -> [a]
arityList Proxy fs
_ = []