{-# language AllowAmbiguousTypes #-}
{-# language DataKinds #-}
{-# language FlexibleInstances #-}
{-# language MultiParamTypeClasses #-}
{-# language PolyKinds #-}
{-# language ScopedTypeVariables #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}

module Rel8.Generic.Record
  ( Record(..)
  , GRecordable, GRecord, grecord, gunrecord
  )
where

-- base
import Data.Kind ( Constraint, Type )
import GHC.Generics
  ( Generic, Rep, from, to
  , (:+:)( L1, R1 ), (:*:)( (:*:) ), M1( M1 )
  , Meta( MetaCons, MetaSel ), D, C, S
  )
import GHC.TypeLits ( type (+), AppendSymbol, Div, Mod, Nat, Symbol )
import Prelude hiding ( Show )


type GRecord :: (Type -> Type) -> Type -> Type
type family GRecord rep where
  GRecord (M1 D meta rep) = M1 D meta (GRecord rep)
  GRecord (l :+: r) = GRecord l :+: GRecord r
  GRecord (M1 C ('MetaCons name fixity 'False) rep) =
    M1 C ('MetaCons name fixity 'True) (Snd (Count 0 rep))
  GRecord rep = rep


type Count :: Nat -> (Type -> Type) -> (Nat, Type -> Type)
type family Count n rep where
  Count n (M1 S ('MetaSel _selector su ss ds) rep) =
    '(n + 1, M1 S ('MetaSel ('Just (Show (n + 1))) su ss ds) rep)
  Count n (a :*: b) = CountHelper1 (Count n a) b
  Count n rep = '(n, rep)


type CountHelper1 :: (Nat, Type -> Type) -> (Type -> Type) -> (Nat, Type -> Type)
type family CountHelper1 tuple b where
  CountHelper1 '(n, a) b = CountHelper2 a (Count n b)


type CountHelper2 :: (Type -> Type) -> (Nat, Type -> Type) -> (Nat, Type -> Type)
type family CountHelper2 a tuple where
  CountHelper2 a '(n, b) = '(n, a :*: b)


type Show :: Nat -> Symbol
type Show n =
  AppendSymbol "_" (AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10)))


type Show' :: Nat -> Symbol
type family Show' n where
  Show' 0 = ""
  Show' n = AppendSymbol (Show' (Div n 10)) (ShowDigit (Mod n 10))


type ShowDigit :: Nat -> Symbol
type family ShowDigit n where
  ShowDigit 0 = "0"
  ShowDigit 1 = "1"
  ShowDigit 2 = "2"
  ShowDigit 3 = "3"
  ShowDigit 4 = "4"
  ShowDigit 5 = "5"
  ShowDigit 6 = "6"
  ShowDigit 7 = "7"
  ShowDigit 8 = "8"
  ShowDigit 9 = "9"


type Snd :: (a, b) -> b
type family Snd tuple where
  Snd '(_a, b) = b


type GRecordable :: (Type -> Type) -> Constraint
class GRecordable rep where
  grecord :: rep x -> GRecord rep x
  gunrecord :: GRecord rep x -> rep x


instance GRecordable rep => GRecordable (M1 D meta rep) where
  grecord :: M1 D meta rep x -> GRecord (M1 D meta rep) x
grecord (M1 rep x
a) = GRecord rep x -> M1 D meta (GRecord rep) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (rep x -> GRecord rep x
forall (rep :: * -> *) x. GRecordable rep => rep x -> GRecord rep x
grecord rep x
a)
  gunrecord :: GRecord (M1 D meta rep) x -> M1 D meta rep x
gunrecord (M1 a) = rep x -> M1 D meta rep x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (GRecord rep x -> rep x
forall (rep :: * -> *) x. GRecordable rep => GRecord rep x -> rep x
gunrecord GRecord rep x
a)


instance (GRecordable l, GRecordable r) => GRecordable (l :+: r) where
  grecord :: (:+:) l r x -> GRecord (l :+: r) x
grecord (L1 l x
a) = GRecord l x -> (:+:) (GRecord l) (GRecord r) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (l x -> GRecord l x
forall (rep :: * -> *) x. GRecordable rep => rep x -> GRecord rep x
grecord l x
a)
  grecord (R1 r x
a) = GRecord r x -> (:+:) (GRecord l) (GRecord r) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (r x -> GRecord r x
forall (rep :: * -> *) x. GRecordable rep => rep x -> GRecord rep x
grecord r x
a)
  gunrecord :: GRecord (l :+: r) x -> (:+:) l r x
gunrecord (L1 a) = l x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (GRecord l x -> l x
forall (rep :: * -> *) x. GRecordable rep => GRecord rep x -> rep x
gunrecord GRecord l x
a)
  gunrecord (R1 a) = r x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (GRecord r x -> r x
forall (rep :: * -> *) x. GRecordable rep => GRecord rep x -> rep x
gunrecord GRecord r x
a)


instance Countable 0 rep =>
  GRecordable (M1 C ('MetaCons name fixity 'False) rep)
 where
  grecord :: M1 C ('MetaCons name fixity 'False) rep x
-> GRecord (M1 C ('MetaCons name fixity 'False) rep) x
grecord (M1 rep x
a) = Snd (Count 0 rep) x
-> M1 C ('MetaCons name fixity 'True) (Snd (Count 0 rep)) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (rep x -> Snd (Count 0 rep) x
forall (n :: Nat) (rep :: * -> *) x.
Countable n rep =>
rep x -> Snd (Count n rep) x
count @0 rep x
a)
  gunrecord :: GRecord (M1 C ('MetaCons name fixity 'False) rep) x
-> M1 C ('MetaCons name fixity 'False) rep x
gunrecord (M1 a) = rep x -> M1 C ('MetaCons name fixity 'False) rep x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Snd (Count 0 rep) x -> rep x
forall (n :: Nat) (rep :: * -> *) x.
Countable n rep =>
Snd (Count n rep) x -> rep x
uncount @0 Snd (Count 0 rep) x
a)


instance {-# OVERLAPPABLE #-} GRecord rep ~ rep => GRecordable rep where
  grecord :: rep x -> GRecord rep x
grecord = rep x -> GRecord rep x
forall a. a -> a
id
  gunrecord :: GRecord rep x -> rep x
gunrecord = GRecord rep x -> rep x
forall a. a -> a
id


type Countable :: Nat -> (Type -> Type) -> Constraint
class Countable n rep where
  count :: rep x -> Snd (Count n rep) x
  uncount :: Snd (Count n rep) x -> rep x


instance Countable n (M1 S ('MetaSel selector su ss ds) rep) where
  count :: M1 S ('MetaSel selector su ss ds) rep x
-> Snd (Count n (M1 S ('MetaSel selector su ss ds) rep)) x
count (M1 rep x
a) = rep x
-> M1
     S
     ('MetaSel
        ('Just
           (AppendSymbol
              "_"
              (AppendSymbol
                 (Show' (Div (n + 1) 10)) (ShowDigit (Mod (n + 1) 10)))))
        su
        ss
        ds)
     rep
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 rep x
a
  uncount :: Snd (Count n (M1 S ('MetaSel selector su ss ds) rep)) x
-> M1 S ('MetaSel selector su ss ds) rep x
uncount (M1 a) = rep x -> M1 S ('MetaSel selector su ss ds) rep x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 rep x
a


instance
  ( Countable n a, Countable n' b
  , '(n', a') ~ Count n a
  , Snd (CountHelper2 a' (Count n' b)) ~ (a' :*: Snd (Count n' b))
  )
  => Countable n (a :*: b)
 where
  count :: (:*:) a b x -> Snd (Count n (a :*: b)) x
count (a x
a :*: b x
b) = a x -> Snd (Count n a) x
forall (n :: Nat) (rep :: * -> *) x.
Countable n rep =>
rep x -> Snd (Count n rep) x
count @n a x
a a' x -> Snd (Count n' b) x -> (:*:) a' (Snd (Count n' b)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b x -> Snd (Count n' b) x
forall (n :: Nat) (rep :: * -> *) x.
Countable n rep =>
rep x -> Snd (Count n rep) x
count @n' b x
b
  uncount :: Snd (Count n (a :*: b)) x -> (:*:) a b x
uncount (a :*: b) = Snd (Count n a) x -> a x
forall (n :: Nat) (rep :: * -> *) x.
Countable n rep =>
Snd (Count n rep) x -> rep x
uncount @n a' x
Snd (Count n a) x
a a x -> b x -> (:*:) a b x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Snd (Count n' b) x -> b x
forall (n :: Nat) (rep :: * -> *) x.
Countable n rep =>
Snd (Count n rep) x -> rep x
uncount @n' Snd (Count n' b) x
b


instance {-# OVERLAPPABLE #-} Snd (Count n rep) ~ rep => Countable n rep where
  count :: rep x -> Snd (Count n rep) x
count = rep x -> Snd (Count n rep) x
forall a. a -> a
id
  uncount :: Snd (Count n rep) x -> rep x
uncount = Snd (Count n rep) x -> rep x
forall a. a -> a
id


newtype Record a = Record
  { Record a -> a
unrecord :: a
  }


instance (Generic a, GRecordable (Rep a)) => Generic (Record a) where
  type Rep (Record a) = GRecord (Rep a)

  from :: Record a -> Rep (Record a) x
from (Record a
a) = Rep a x -> GRecord (Rep a) x
forall (rep :: * -> *) x. GRecordable rep => rep x -> GRecord rep x
grecord (a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
a)
  to :: Rep (Record a) x -> Record a
to = a -> Record a
forall a. a -> Record a
Record (a -> Record a)
-> (GRecord (Rep a) x -> a) -> GRecord (Rep a) x -> Record a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a x -> a
forall a x. Generic a => Rep a x -> a
to (Rep a x -> a)
-> (GRecord (Rep a) x -> Rep a x) -> GRecord (Rep a) x -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GRecord (Rep a) x -> Rep a x
forall (rep :: * -> *) x. GRecordable rep => GRecord rep x -> rep x
gunrecord