{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
module Generics.SOP.Record
  ( -- * A suitable representation for single-constructor records
    FieldLabel
  , RecordCode
  , Record
  , RecordRep
    -- * Computing the record code
  , RecordCodeOf
  , IsRecord
  , ValidRecordCode
  , ExtractTypesFromRecordCode
  , ExtractLabelsFromRecordCode
  , RecombineRecordCode
    -- * Conversion between a type and its record representation.
  , toRecord
  , fromRecord
    -- * Utilities
  , 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

--------------------------------------------------------------------------
-- A suitable representation for single-constructor records.
--------------------------------------------------------------------------

-- | On the type-level, we represent fiel labels using symbols.
type FieldLabel = Symbol

-- | The record code deviates from the normal SOP code in two
-- ways:
--
-- - There is only one list, because we require that there is
--   only a single constructor.
--
-- - In addition to the types of the fields, we store the labels
--   of the fields.
--
type RecordCode = [(FieldLabel, Type)]

-- | The record representation of a type is a record indexed
-- by the record code.
--
type RecordRep (a :: Type) = Record (RecordCodeOf a)

-- | The representation of a record is just a product indexed by
-- a record code, containing elements of the types indicated
-- by the code.
--
-- Note that the representation is deliberately chosen such that
-- it has the same run-time representation as the product part
-- of the normal SOP representation.
--
type Record (r :: RecordCode) = NP P r

--------------------------------------------------------------------------
-- Computing the record code
--------------------------------------------------------------------------

-- | This type-level function takes the type-level metadata provided
-- by generics-sop as well as the normal generics-sop code, and transforms
-- them into the record code.
--
-- Arguably, the record code is more usable than the representation
-- directly on offer by generics-sop. So it's worth asking whether
-- this representation should be included in generics-sop ...
--
-- The function will only reduce if the argument type actually is a
-- record, meaning it must have exactly one constructor, and that
-- constructor must have field labels attached to it.
--
type RecordCodeOf a = ToRecordCode_Datatype a (DatatypeInfoOf a) (Code a)

-- | Helper for 'RecordCodeOf', handling the datatype level. Both
-- datatypes and newtypes are acceptable. Newtypes are just handled
-- as one-constructor datatypes for this purpose.
--
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

-- | Helper for 'RecordCodeOf', handling the constructor level. Only
-- single-constructor types are acceptable, and the constructor must
-- contain field labels.
--
-- As an exception, we accept an empty record, even though it does
-- not explicitly define any field labels.
--
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."
      )

-- | Helper for 'RecordCodeOf', handling the field level. At this point,
-- we simply zip the list of field names and the list of types.
--
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

-- * Relating the record code and the original code.

-- | The constraint @IsRecord a r@ states that the type 'a' is a record type
-- (i.e., has exactly one constructor and field labels) and that 'r' is the
-- record code associated with 'a'.
--
type IsRecord (a :: Type) (r :: RecordCode) =
  IsRecord' a r (GetSingleton (Code a))

-- | The constraint @IsRecord' a r xs@ states that 'a' is a record type
-- with record code 'r', and that the types contained in 'r' correspond
-- to the list 'xs'.
--
-- If the record code computation is correct, then the record code of a
-- type is strongly related to the original generics-sop code. Extracting
-- the types out of 'r' should correspond to 'xs'. Recombining the
-- labels from 'r' with 'xs' should yield 'r' exactly. These sanity
-- properties are captured by 'ValidRecordCode'.
--
type IsRecord' (a :: Type) (r :: RecordCode) (xs :: [Type]) =
  ( Generic a, Code a ~ '[ xs ]
  , RecordCodeOf a ~ r, ValidRecordCode r xs
  )

-- | Relates a recordcode 'r' and a list of types 'xs', stating that
-- 'xs' is indeed the list of types contained in 'r'.
--
type ValidRecordCode (r :: RecordCode) (xs :: [Type]) =
  ( ExtractTypesFromRecordCode r ~ xs
  , RecombineRecordCode (ExtractLabelsFromRecordCode r) xs ~ r
  )

-- | Extracts all the types from a record code.
type family ExtractTypesFromRecordCode (r :: RecordCode) :: [Type] where
  ExtractTypesFromRecordCode '[]             = '[]
  ExtractTypesFromRecordCode ( '(_, a) : r ) = a : ExtractTypesFromRecordCode r

-- | Extracts all the field labels from a record code.
type family ExtractLabelsFromRecordCode (r :: RecordCode) :: [FieldLabel] where
  ExtractLabelsFromRecordCode '[]             = '[]
  ExtractLabelsFromRecordCode ( '(l, _) : r ) = l : ExtractLabelsFromRecordCode r

-- | Given a list of labels and types, recombines them into a record code.
--
-- An important aspect of this function is that it is defined by induction
-- on the list of types, and forces the list of field labels to be at least
-- as long.
--
type family RecombineRecordCode (ls :: [FieldLabel]) (ts :: [Type]) :: RecordCode where
  RecombineRecordCode _ '[]       = '[]
  RecombineRecordCode ls (t : ts) = '(Head ls, t) : RecombineRecordCode (Tail ls) ts

--------------------------------------------------------------------------
-- Conversion between a type and its record representation.
--------------------------------------------------------------------------

-- | Convert a value into its record representation.
toRecord :: (IsRecord a _r) => a -> RecordRep a
toRecord :: a -> RecordRep a
toRecord = NP I (GetSingleton (Code a)) -> Record _r
forall (r :: RecordCode) (xs :: [*]).
ValidRecordCode r xs =>
NP I xs -> Record r
unsafeToRecord_NP (NP I (GetSingleton (Code a)) -> Record _r)
-> (a -> NP I (GetSingleton (Code a))) -> a -> Record _r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS (NP I) '[GetSingleton (Code a)] -> NP I (GetSingleton (Code a))
forall k (f :: k -> *) (x :: k). NS f '[x] -> f x
unZ (NS (NP I) '[GetSingleton (Code a)]
 -> NP I (GetSingleton (Code a)))
-> (a -> NS (NP I) '[GetSingleton (Code a)])
-> a
-> NP I (GetSingleton (Code a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP I '[GetSingleton (Code a)]
-> NS (NP I) '[GetSingleton (Code a)]
forall k (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
unSOP (SOP I '[GetSingleton (Code a)]
 -> NS (NP I) '[GetSingleton (Code a)])
-> (a -> SOP I '[GetSingleton (Code a)])
-> a
-> NS (NP I) '[GetSingleton (Code a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SOP I '[GetSingleton (Code a)]
forall a. Generic a => a -> Rep a
from

-- | Convert an n-ary product into the corresponding record
-- representation. This is a no-op, and more efficiently
-- implented using 'unsafeToRecord_NP'. It is included here
-- to demonstrate that it actually is type-correct and also
-- to make it more obvious that it is indeed a no-op.
--
_toRecord_NP :: (ValidRecordCode r xs) => NP I xs -> Record r
_toRecord_NP :: NP I xs -> Record r
_toRecord_NP NP I xs
Nil         = Record r
forall k (a :: k -> *). NP a '[]
Nil
_toRecord_NP (I x
x :* NP I xs
xs) = Snd '(Head (ExtractLabelsFromRecordCode r), x)
-> P '(Head (ExtractLabelsFromRecordCode r), x)
forall a (p :: (a, *)). Snd p -> P p
P x
Snd '(Head (ExtractLabelsFromRecordCode r), x)
x P '(Head (ExtractLabelsFromRecordCode r), x)
-> NP
     P (RecombineRecordCode (Tail (ExtractLabelsFromRecordCode r)) xs)
-> NP
     P
     ('(Head (ExtractLabelsFromRecordCode r), x)
        : RecombineRecordCode (Tail (ExtractLabelsFromRecordCode r)) xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I xs
-> NP
     P (RecombineRecordCode (Tail (ExtractLabelsFromRecordCode r)) xs)
forall (r :: RecordCode) (xs :: [*]).
ValidRecordCode r xs =>
NP I xs -> Record r
_toRecord_NP NP I xs
xs

-- | Fast version of 'toRecord_NP'. Not actually unsafe as
-- long as the internal representations of 'NP' and 'Record'
-- are not changed.
--
unsafeToRecord_NP :: (ValidRecordCode r xs) => NP I xs -> Record r
unsafeToRecord_NP :: NP I xs -> Record r
unsafeToRecord_NP = NP I xs -> Record r
forall a b. a -> b
unsafeCoerce

-- | Convert a record representation back into a value.
fromRecord :: (IsRecord a r) => RecordRep a -> a
fromRecord :: RecordRep a -> a
fromRecord = SOP I '[GetSingleton (Code a)] -> a
forall a. Generic a => Rep a -> a
to (SOP I '[GetSingleton (Code a)] -> a)
-> (Record r -> SOP I '[GetSingleton (Code a)]) -> Record r -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS (NP I) '[GetSingleton (Code a)]
-> SOP I '[GetSingleton (Code a)]
forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
SOP (NS (NP I) '[GetSingleton (Code a)]
 -> SOP I '[GetSingleton (Code a)])
-> (Record r -> NS (NP I) '[GetSingleton (Code a)])
-> Record r
-> SOP I '[GetSingleton (Code a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP I (GetSingleton (Code a)) -> NS (NP I) '[GetSingleton (Code a)]
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (NP I (GetSingleton (Code a))
 -> NS (NP I) '[GetSingleton (Code a)])
-> (Record r -> NP I (GetSingleton (Code a)))
-> Record r
-> NS (NP I) '[GetSingleton (Code a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record r -> NP I (GetSingleton (Code a))
forall (r :: RecordCode) (xs :: [*]).
(ValidRecordCode r xs, SListI xs) =>
Record r -> NP I xs
unsafeFromRecord_NP

-- | Convert a record representation into an n-ary product. This is a no-op,
-- and more efficiently implemented using 'unsafeFromRecord_NP'.
--
-- It is also noteworthy that we let the resulting list drive the computation.
-- This is compatible with the definition of 'RecombineRecordCode' based on
-- the list of types.
--
_fromRecord_NP :: forall r xs . (ValidRecordCode r xs, SListI xs) => Record r -> NP I xs
_fromRecord_NP :: Record r -> NP I xs
_fromRecord_NP = case SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList :: SList xs of
  SList xs
SNil  -> NP I '[] -> Record r -> NP I '[]
forall a b. a -> b -> a
const NP I '[]
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 -> x -> I x
forall a. a -> I a
I x
Snd x
x I x -> NP I xs -> NP I (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP P xs -> NP I xs
forall (r :: RecordCode) (xs :: [*]).
(ValidRecordCode r xs, SListI xs) =>
Record r -> NP I xs
_fromRecord_NP NP P xs
xs

-- | Fast version of 'fromRecord_NP'. Not actually unsafe as
-- long as the internal representation of 'NP' and 'Record'
-- are not changed.
--
unsafeFromRecord_NP :: forall r xs . (ValidRecordCode r xs, SListI xs) => Record r -> NP I xs
unsafeFromRecord_NP :: Record r -> NP I xs
unsafeFromRecord_NP = Record r -> NP I xs
forall a b. a -> b
unsafeCoerce

--------------------------------------------------------------------------
-- Utilities
--------------------------------------------------------------------------

-- | Projection of the second component of a type-level pair,
-- wrapped in a newtype.
--
newtype P (p :: (a, Type)) = P (Snd p)
  deriving ((forall x. P p -> Rep (P p) x)
-> (forall x. Rep (P p) x -> P p) -> Generic (P p)
forall x. Rep (P p) x -> P p
forall x. P p -> Rep (P p) x
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) = a -> ()
forall a. NFData a => a -> ()
rnf a
Snd '(l, a)
x

-- | Type-level variant of 'snd'.
type family Snd (p :: (a, b)) :: b where
  Snd '(a, b) = b

-- | Type-level variant of 'head'.
type family Head (xs :: [k]) :: k where
  Head (x : xs) = x

-- | Type-level variant of 'tail'.
type family Tail (xs :: [k]) :: [k] where
  Tail (x : xs) = xs

-- | Partial type-level function that extracts the only element
-- from a singleton type-level list.
--
type family GetSingleton (xs :: [k]) :: k where
  GetSingleton '[ x ] = x