{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
#if MIN_VERSION_base(4,12,0)
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
#else
{-# LANGUAGE TypeInType #-}
#endif
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Generics.SOP.Record
(
FieldLabel
, RecordCode
, Record
, RecordRep
, RecordCodeOf
, IsRecord
, ValidRecordCode
, ExtractTypesFromRecordCode
, ExtractLabelsFromRecordCode
, RecombineRecordCode
, toRecord
, fromRecord
, P(..)
, Snd
)
where
import Control.DeepSeq
import Generics.SOP.BasicFunctors
import Generics.SOP.NP
import Generics.SOP.NS
import Generics.SOP.Universe
import Generics.SOP.Sing
import Generics.SOP.Type.Metadata
import qualified GHC.Generics as GHC
import GHC.TypeLits
import GHC.Types
import Unsafe.Coerce
type FieldLabel = Symbol
type RecordCode = [(FieldLabel, Type)]
type RecordRep (a :: Type) = Record (RecordCodeOf a)
type Record (r :: RecordCode) = NP P r
type RecordCodeOf a = ToRecordCode_Datatype a (DatatypeInfoOf a) (Code a)
type family
ToRecordCode_Datatype (a :: Type) (d :: DatatypeInfo) (c :: [[Type]]) :: RecordCode where
#if MIN_VERSION_generics_sop(0,5,0)
ToRecordCode_Datatype a (ADT _ _ cis _) c = ToRecordCode_Constructor a cis c
#else
ToRecordCode_Datatype a (ADT _ _ cis) c = ToRecordCode_Constructor a cis c
#endif
ToRecordCode_Datatype a (Newtype _ _ ci) c = ToRecordCode_Constructor a '[ ci ] c
type family
ToRecordCode_Constructor (a :: Type) (cis :: [ConstructorInfo]) (c :: [[Type]]) :: RecordCode where
ToRecordCode_Constructor a '[ 'Record _ fis ] '[ ts ] = ToRecordCode_Field fis ts
ToRecordCode_Constructor a '[ 'Constructor _ ] '[ '[] ] = '[]
ToRecordCode_Constructor a '[] _ =
TypeError
( Text "The type `" :<>: ShowType a :<>: Text "' is not a record type."
:$$: Text "It has no constructors."
)
ToRecordCode_Constructor a ( _ : _ : _ ) _ =
TypeError
( Text "The type `" :<>: ShowType a :<>: Text "' is not a record type."
:$$: Text "It has more than one constructor."
)
ToRecordCode_Constructor a '[ _ ] _ =
TypeError
( Text "The type `" :<>: ShowType a :<>: Text "' is not a record type."
:$$: Text "It has no labelled fields."
)
type family ToRecordCode_Field (fis :: [FieldInfo]) (c :: [Type]) :: RecordCode where
ToRecordCode_Field '[] '[] = '[]
ToRecordCode_Field ( 'FieldInfo l : fis ) ( t : ts ) = '(l, t) : ToRecordCode_Field fis ts
type IsRecord (a :: Type) (r :: RecordCode) =
IsRecord' a r (GetSingleton (Code a))
type IsRecord' (a :: Type) (r :: RecordCode) (xs :: [Type]) =
( Generic a, Code a ~ '[ xs ]
, RecordCodeOf a ~ r, ValidRecordCode r xs
)
type ValidRecordCode (r :: RecordCode) (xs :: [Type]) =
( ExtractTypesFromRecordCode r ~ xs
, RecombineRecordCode (ExtractLabelsFromRecordCode r) xs ~ r
)
type family (r :: RecordCode) :: [Type] where
'[] = '[]
( '(_, a) : r ) = a : ExtractTypesFromRecordCode r
type family (r :: RecordCode) :: [FieldLabel] where
'[] = '[]
( '(l, _) : r ) = l : ExtractLabelsFromRecordCode r
type family RecombineRecordCode (ls :: [FieldLabel]) (ts :: [Type]) :: RecordCode where
RecombineRecordCode _ '[] = '[]
RecombineRecordCode ls (t : ts) = '(Head ls, t) : RecombineRecordCode (Tail ls) ts
toRecord :: (IsRecord a _r) => a -> RecordRep a
toRecord :: forall a (_r :: RecordCode). IsRecord a _r => a -> RecordRep a
toRecord = forall (r :: RecordCode) (xs :: [*]).
ValidRecordCode r xs =>
NP I xs -> Record r
unsafeToRecord_NP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (x :: k). NS f '[x] -> f x
unZ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
unSOP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Generic a => a -> Rep a
from
_toRecord_NP :: (ValidRecordCode r xs) => NP I xs -> Record r
_toRecord_NP :: forall (r :: RecordCode) (xs :: [*]).
ValidRecordCode r xs =>
NP I xs -> Record r
_toRecord_NP NP I xs
Nil = forall {k} (a :: k -> *). NP a '[]
Nil
_toRecord_NP (I x
x :* NP I xs
xs) = forall a (p :: (a, *)). Snd p -> P p
P x
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall (r :: RecordCode) (xs :: [*]).
ValidRecordCode r xs =>
NP I xs -> Record r
_toRecord_NP NP I xs
xs
unsafeToRecord_NP :: (ValidRecordCode r xs) => NP I xs -> Record r
unsafeToRecord_NP :: forall (r :: RecordCode) (xs :: [*]).
ValidRecordCode r xs =>
NP I xs -> Record r
unsafeToRecord_NP = forall a b. a -> b
unsafeCoerce
fromRecord :: forall a r . (IsRecord a r) => RecordRep a -> a
fromRecord :: forall a (r :: RecordCode). IsRecord a r => RecordRep a -> a
fromRecord = forall (xs :: [*]). IsRecord' a r xs => RecordRep a -> a
fromRecord'
where
fromRecord' :: forall xs . (IsRecord' a r xs) => RecordRep a -> a
fromRecord' :: forall (xs :: [*]). IsRecord' a r xs => RecordRep a -> a
fromRecord' = forall a. Generic a => Rep a -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: RecordCode) (xs :: [*]).
(ValidRecordCode r xs, SListI xs) =>
Record r -> NP I xs
unsafeFromRecord_NP
_fromRecord_NP :: forall r xs . (ValidRecordCode r xs, SListI xs) => Record r -> NP I xs
_fromRecord_NP :: forall (r :: RecordCode) (xs :: [*]).
(ValidRecordCode r xs, SListI xs) =>
Record r -> NP I xs
_fromRecord_NP = case forall {k} (xs :: [k]). SListI xs => SList xs
sList :: SList xs of
SList xs
SNil -> forall a b. a -> b -> a
const forall {k} (a :: k -> *). NP a '[]
Nil
SList xs
SCons -> \ Record r
r -> case Record r
r of
P Snd x
x :* NP P xs
xs -> forall a. a -> I a
I Snd x
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall (r :: RecordCode) (xs :: [*]).
(ValidRecordCode r xs, SListI xs) =>
Record r -> NP I xs
_fromRecord_NP NP P xs
xs
unsafeFromRecord_NP :: forall r xs . (ValidRecordCode r xs, SListI xs) => Record r -> NP I xs
unsafeFromRecord_NP :: forall (r :: RecordCode) (xs :: [*]).
(ValidRecordCode r xs, SListI xs) =>
Record r -> NP I xs
unsafeFromRecord_NP = forall a b. a -> b
unsafeCoerce
newtype P (p :: (a, Type)) = P (Snd p)
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a (p :: (a, *)) x. Rep (P p) x -> P p
forall a (p :: (a, *)) x. P p -> Rep (P p) x
$cto :: forall a (p :: (a, *)) x. Rep (P p) x -> P p
$cfrom :: forall a (p :: (a, *)) x. P p -> Rep (P p) x
GHC.Generic)
deriving instance Eq a => Eq (P '(l, a))
deriving instance Ord a => Ord (P '(l, a))
deriving instance Show a => Show (P '(l, a))
instance NFData a => NFData (P '(l, a)) where
rnf :: P '(l, a) -> ()
rnf (P Snd '(l, a)
x) = forall a. NFData a => a -> ()
rnf Snd '(l, a)
x
type family Snd (p :: (a, b)) :: b where
Snd '(a, b) = b
type family Head (xs :: [k]) :: k where
Head (x : xs) = x
type family Tail (xs :: [k]) :: [k] where
Tail (x : xs) = xs
type family GetSingleton (xs :: [k]) :: k where
GetSingleton '[ x ] = x