{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Generic.HKD.Named
( Record (..)
) where
import Data.Functor.Contravariant (Contravariant (..))
import Data.Generic.HKD.Types (HKD, HKD_)
import Data.Generics.Product.Internal.Subtype (GUpcast (..))
import Data.Kind (Type)
import GHC.Generics
import Named ((:!), NamedF (..))
type family Append (xs :: Type -> Type) (ys :: Type -> Type) :: Type -> Type where
Append (S1 meta head) tail = S1 meta head :*: tail
Append (left :*: right) other = left :*: Append right other
type family Rearrange (i :: Type -> Type) :: Type -> Type where
Rearrange (S1 m inner) = S1 m (Rearrange inner)
Rearrange (M1 index m inner) = M1 index m (Rearrange inner)
Rearrange (left :*: right) = Append (Rearrange left) (Rearrange right)
Rearrange (Rec0 inner) = Rec0 inner
class Record (structure :: Type) (f :: Type -> Type) (k :: Type)
| f structure -> k where
record :: k
class GRecord (rep :: Type -> Type) (f :: Type -> Type) (structure :: Type) (k :: Type)
| f structure rep -> k where
grecord :: (forall p. rep p -> HKD structure f) -> k
instance GRecord inner f structure k
=> GRecord (D1 meta inner) f structure k where
grecord :: (forall p. D1 meta inner p -> HKD structure f) -> k
grecord forall p. D1 meta inner p -> HKD structure f
rebuild = forall (rep :: * -> *) (f :: * -> *) structure k.
GRecord rep f structure k =>
(forall p. rep p -> HKD structure f) -> k
grecord (forall p. D1 meta inner p -> HKD structure f
rebuild forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)
instance GRecord inner f structure k
=> GRecord (C1 meta inner) f structure k where
grecord :: (forall p. C1 meta inner p -> HKD structure f) -> k
grecord forall p. C1 meta inner p -> HKD structure f
rebuild = forall (rep :: * -> *) (f :: * -> *) structure k.
GRecord rep f structure k =>
(forall p. rep p -> HKD structure f) -> k
grecord (forall p. C1 meta inner p -> HKD structure f
rebuild forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)
instance
( rec ~ (Rec0 inner)
, k ~ (name :! inner -> HKD structure f)
, meta ~ 'MetaSel ('Just name) i d c
)
=> GRecord (S1 meta rec) f structure k where
grecord :: (forall p. S1 meta rec p -> HKD structure f) -> k
grecord forall p. S1 meta rec p -> HKD structure f
fill = \(Arg inner
inner) -> forall p. S1 meta rec p -> HKD structure f
fill (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k i c (p :: k). c -> K1 i c p
K1 inner
inner))
instance
( GRecord right f structure k'
, rec ~ Rec0 x
, left ~ S1 ('MetaSel ('Just name) i d c) rec
, k ~ (name :! x -> k')
)
=> GRecord (left :*: right) f structure k where
grecord :: (forall p. (:*:) left right p -> HKD structure f) -> k
grecord forall p. (:*:) left right p -> HKD structure f
fill = \(Arg x
left) -> forall (rep :: * -> *) (f :: * -> *) structure k.
GRecord rep f structure k =>
(forall p. rep p -> HKD structure f) -> k
grecord \right p
right -> forall p. (:*:) left right p -> HKD structure f
fill (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k i c (p :: k). c -> K1 i c p
K1 x
left) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: right p
right)
instance
( Contravariant (HKD_ f structure)
, Functor (HKD_ f structure)
, list ~ Rearrange (HKD_ f structure)
, GUpcast list (HKD_ f structure)
, GRecord list f structure k
)
=> Record structure f k where
record :: k
record = forall (rep :: * -> *) (f :: * -> *) structure k.
GRecord rep f structure k =>
(forall p. rep p -> HKD structure f) -> k
grecord @_ @f @structure (forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (sub :: * -> *) (sup :: * -> *) p.
GUpcast sub sup =>
sub p -> sup p
gupcast @list @(HKD_ f structure))