{-# LANGUAGE UndecidableInstances #-} -- required for TypeError >:(

module Binrep.Generic.BLen where

import GHC.Generics
import GHC.TypeLits ( TypeError )

import Binrep.BLen
import Binrep.Generic.Internal
import Util.Generic

blenGeneric :: (Generic a, GBLen (Rep a), BLen w) => Cfg w -> a -> BLenT
blenGeneric :: forall a w.
(Generic a, GBLen (Rep a), BLen w) =>
Cfg w -> a -> BLenT
blenGeneric Cfg w
cfg = forall {k} (f :: k -> *) w (p :: k).
(GBLen f, BLen w) =>
Cfg w -> f p -> BLenT
gblen Cfg w
cfg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => a -> Rep a x
from

class GBLen f where
    gblen :: BLen w => Cfg w -> f p -> BLenT

-- | Empty constructor.
instance GBLen U1 where
    gblen :: forall w (p :: k). BLen w => Cfg w -> U1 p -> BLenT
gblen Cfg w
_ U1 p
U1 = BLenT
0

-- | Field.
instance BLen c => GBLen (K1 i c) where
    gblen :: forall w (p :: k). BLen w => Cfg w -> K1 i c p -> BLenT
gblen Cfg w
_ (K1 c
c) = forall a. BLen a => a -> BLenT
blen c
c

-- | Product type fields are consecutive.
instance (GBLen l, GBLen r) => GBLen (l :*: r) where
    gblen :: forall w (p :: k). BLen w => Cfg w -> (:*:) l r p -> BLenT
gblen Cfg w
cfg (l p
l :*: r p
r) = forall {k} (f :: k -> *) w (p :: k).
(GBLen f, BLen w) =>
Cfg w -> f p -> BLenT
gblen Cfg w
cfg l p
l forall a. Num a => a -> a -> a
+ forall {k} (f :: k -> *) w (p :: k).
(GBLen f, BLen w) =>
Cfg w -> f p -> BLenT
gblen Cfg w
cfg r p
r

-- | Constructor sums are differentiated by a prefix tag.
instance GBLenSum (l :+: r) => GBLen (l :+: r) where
    gblen :: forall w (p :: k). BLen w => Cfg w -> (:+:) l r p -> BLenT
gblen = forall {k} (f :: k -> *) w (p :: k).
(GBLenSum f, BLen w) =>
Cfg w -> f p -> BLenT
gblensum

-- | Refuse to derive instance for void datatype.
instance TypeError GErrRefuseVoid => GBLen V1 where
    gblen :: forall w (p :: k). BLen w => Cfg w -> V1 p -> BLenT
gblen = forall a. HasCallStack => a
undefined

-- | Any datatype, constructor or record.
instance GBLen f => GBLen (M1 i d f) where
    gblen :: forall w (p :: k). BLen w => Cfg w -> M1 i d f p -> BLenT
gblen Cfg w
cfg = forall {k} (f :: k -> *) w (p :: k).
(GBLen f, BLen w) =>
Cfg w -> f p -> BLenT
gblen Cfg w
cfg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

--------------------------------------------------------------------------------

class GBLenSum f where
    gblensum :: BLen w => Cfg w -> f p -> BLenT

instance (GBLenSum l, GBLenSum r) => GBLenSum (l :+: r) where
    gblensum :: forall w (p :: k). BLen w => Cfg w -> (:+:) l r p -> BLenT
gblensum Cfg w
cfg = \case L1 l p
l -> forall {k} (f :: k -> *) w (p :: k).
(GBLenSum f, BLen w) =>
Cfg w -> f p -> BLenT
gblensum Cfg w
cfg l p
l
                         R1 r p
r -> forall {k} (f :: k -> *) w (p :: k).
(GBLenSum f, BLen w) =>
Cfg w -> f p -> BLenT
gblensum Cfg w
cfg r p
r

instance (GBLen f, Constructor c) => GBLenSum (C1 c f) where
    gblensum :: forall w (p :: k). BLen w => Cfg w -> C1 c f p -> BLenT
gblensum Cfg w
cfg C1 c f p
x = forall a. BLen a => a -> BLenT
blen ((forall a. Cfg a -> String -> a
cSumTag Cfg w
cfg) (forall {k} (c :: k). Constructor c => String
conName' @c)) forall a. Num a => a -> a -> a
+ forall {k} (f :: k -> *) w (p :: k).
(GBLen f, BLen w) =>
Cfg w -> f p -> BLenT
gblen Cfg w
cfg (forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 C1 c f p
x)