{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE KindSignatures          #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE QuantifiedConstraints   #-}
{-# LANGUAGE ScopedTypeVariables     #-}
{-# LANGUAGE StandaloneDeriving      #-}
{-# LANGUAGE TypeApplications        #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- | Interop with @generics-sop@ generics
module Data.Record.Generic.SOP (
    -- | Translate between SOP representation and large-records representation
    Field(..)
  , fromSOP
  , toSOP
    -- | Translate constraints
  , toDictAll
    -- | Additional SOP functions
  , glowerBound
  ) where

import Data.Kind
import Data.Proxy
import Data.SOP.Dict (all_NP)
import Generics.SOP (SOP(..), NS(..), NP(..), SListI, All, Code, Compose)
import GHC.Exts (Any)
import GHC.TypeLits (Symbol)

import qualified Data.Vector  as V
import qualified Generics.SOP as SOP

import Data.Record.Generic
import Data.Record.Generic.LowerBound hiding (glowerBound)
import Data.Record.TH.Runtime (noInlineUnsafeCo)

{-------------------------------------------------------------------------------
  Conversion back and forth to generics-sop records

  NOTE: We do /not/ require @SListI (MetadataOf a)@ by default, as this would
  result in quadratic blow-up again. This is only required in this module for
  SOP interop.

  NOTE: We don't currently use @records-sop@, despite it being a /near/ perfect
  fit. The problem is that @records-sop@ is not generalized over a functor,
  which would make these functions less general than we need them to be.
-------------------------------------------------------------------------------}

newtype Field (f :: Type -> Type) (field :: (Symbol, Type)) where
  Field :: f (FieldType field) -> Field f field

deriving instance Show (f x) => Show (Field f '(nm, x))
deriving instance Eq   (f x) => Eq   (Field f '(nm, x))

fromSOP :: SListI (MetadataOf a) => NP (Field f) (MetadataOf a) -> Rep f a
fromSOP :: NP (Field f) (MetadataOf a) -> Rep f a
fromSOP =
    Vector (f Any) -> Rep f a
forall (f :: Type -> Type) a. Vector (f Any) -> Rep f a
Rep (Vector (f Any) -> Rep f a)
-> (NP (Field f) (MetadataOf a) -> Vector (f Any))
-> NP (Field f) (MetadataOf a)
-> Rep f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [f Any] -> Vector (f Any)
forall a. [a] -> Vector a
V.fromList ([f Any] -> Vector (f Any))
-> (NP (Field f) (MetadataOf a) -> [f Any])
-> NP (Field f) (MetadataOf a)
-> Vector (f Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K (f Any)) (MetadataOf a) -> [f Any]
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
SOP.hcollapse (NP (K (f Any)) (MetadataOf a) -> [f Any])
-> (NP (Field f) (MetadataOf a) -> NP (K (f Any)) (MetadataOf a))
-> NP (Field f) (MetadataOf a)
-> [f Any]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: (Symbol, Type)). Field f a -> K (f Any) a)
-> NP (Field f) (MetadataOf a) -> NP (K (f Any)) (MetadataOf a)
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l)
       (f :: k -> Type) (f' :: k -> Type).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
SOP.hmap forall (a :: (Symbol, Type)). Field f a -> K (f Any) a
forall (f :: Type -> Type) (field :: (Symbol, Type)).
Field f field -> K (f Any) field
conv
  where
    conv :: Field f field -> K (f Any) field
    conv :: Field f field -> K (f Any) field
conv (Field f (FieldType field)
fx) = f Any -> K (f Any) field
forall k a (b :: k). a -> K a b
K (f Any -> K (f Any) field) -> f Any -> K (f Any) field
forall a b. (a -> b) -> a -> b
$ f (FieldType field) -> f Any
forall a b. a -> b
noInlineUnsafeCo f (FieldType field)
fx

toSOP :: SListI (MetadataOf a) => Rep f a -> Maybe (NP (Field f) (MetadataOf a))
toSOP :: Rep f a -> Maybe (NP (Field f) (MetadataOf a))
toSOP (Rep Vector (f Any)
v) =
    (forall (a :: (Symbol, Type)). K (f Any) a -> Field f a)
-> NP (K (f Any)) (MetadataOf a) -> NP (Field f) (MetadataOf a)
forall k l (h :: (k -> Type) -> l -> Type) (xs :: l)
       (f :: k -> Type) (f' :: k -> Type).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
SOP.hmap forall (a :: (Symbol, Type)). K (f Any) a -> Field f a
forall (f :: Type -> Type) (field :: (Symbol, Type)).
K (f Any) field -> Field f field
conv (NP (K (f Any)) (MetadataOf a) -> NP (Field f) (MetadataOf a))
-> Maybe (NP (K (f Any)) (MetadataOf a))
-> Maybe (NP (Field f) (MetadataOf a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [f Any] -> Maybe (NP (K (f Any)) (MetadataOf a))
forall k (xs :: [k]) a. SListI xs => [a] -> Maybe (NP (K a) xs)
SOP.fromList (Vector (f Any) -> [f Any]
forall a. Vector a -> [a]
V.toList Vector (f Any)
v)
  where
    conv :: K (f Any) field -> Field f field
    conv :: K (f Any) field -> Field f field
conv (K f Any
fx) = f (FieldType field) -> Field f field
forall (f :: Type -> Type) (field :: (Symbol, Type)).
f (FieldType field) -> Field f field
Field (f Any -> f (FieldType field)
forall a b. a -> b
noInlineUnsafeCo f Any
fx)

{-------------------------------------------------------------------------------
  Translate constraints
-------------------------------------------------------------------------------}

-- | Translate constraints
--
-- When using 'toSOP', if you start with something of type
--
-- > Rep f a
--
-- you end up with something of type
--
-- > NP (Field f) (MetadataOf a)
--
-- When doing so, 'toDictAll' can translate
--
-- > Constraints a (Compose c f)
--
-- (which is useful over the original representation) to
--
-- > All (Compose c (Field f)) (MetadataOf a)
--
-- which is useful for the translated representation.
toDictAll ::
     forall f a c.
     ( Generic a
     , Constraints a (Compose c f)
     , All IsField (MetadataOf a)
     , forall nm x. c (f x) => c (Field f '(nm, x))
     )
  => Proxy f
  -> Proxy a
  -> Proxy c
  -> Dict (All (Compose c (Field f))) (MetadataOf a)
toDictAll :: Proxy f
-> Proxy a
-> Proxy c
-> Dict (All (Compose c (Field f))) (MetadataOf a)
toDictAll Proxy f
_ Proxy a
_ Proxy c
_ =
    case Rep (Dict (Compose c f)) a
-> Maybe (NP (Field (Dict (Compose c f))) (MetadataOf a))
forall a (f :: Type -> Type).
SListI (MetadataOf a) =>
Rep f a -> Maybe (NP (Field f) (MetadataOf a))
toSOP Rep (Dict (Compose c f)) a
dictT of
      Maybe (NP (Field (Dict (Compose c f))) (MetadataOf a))
Nothing -> String -> Dict (All (Compose c (Field f))) (MetadataOf a)
forall a. HasCallStack => String -> a
error String
"toDictAll: invalid dictionary"
      Just NP (Field (Dict (Compose c f))) (MetadataOf a)
d  -> NP (Dict (Compose c (Field f))) (MetadataOf a)
-> Dict (All (Compose c (Field f))) (MetadataOf a)
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP (Proxy IsField
-> (forall (a :: (Symbol, Type)).
    IsField a =>
    Field (Dict (Compose c f)) a -> Dict (Compose c (Field f)) a)
-> NP (Field (Dict (Compose c f))) (MetadataOf a)
-> NP (Dict (Compose c (Field f))) (MetadataOf a)
forall k l (h :: (k -> Type) -> l -> Type) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> Type) (f :: k -> Type)
       (f' :: k -> Type).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
SOP.hcmap (Proxy IsField
forall k (t :: k). Proxy t
Proxy @IsField) forall (a :: (Symbol, Type)).
IsField a =>
Field (Dict (Compose c f)) a -> Dict (Compose c (Field f)) a
conv NP (Field (Dict (Compose c f))) (MetadataOf a)
d)
  where
    dictT :: Rep (Dict (Compose c f)) a
    dictT :: Rep (Dict (Compose c f)) a
dictT = Proxy (Compose c f) -> Rep (Dict (Compose c f)) a
forall a (c :: Type -> Constraint).
(Generic a, Constraints a c) =>
Proxy c -> Rep (Dict c) a
dict (Proxy (Compose c f)
forall k (t :: k). Proxy t
Proxy @(Compose c f))

    conv :: IsField field
         => Field (Dict (Compose c f)) field
         -> Dict (Compose c (Field f)) field
    conv :: Field (Dict (Compose c f)) field
-> Dict (Compose c (Field f)) field
conv (Field Dict (Compose c f) (FieldType field)
Dict) = Dict (Compose c (Field f)) field
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

{-------------------------------------------------------------------------------
  Additional SOP generic functions
-------------------------------------------------------------------------------}

glowerBound :: (SOP.Generic a, All LowerBound xs, Code a ~ '[xs]) => a
glowerBound :: a
glowerBound = SOP I '[xs] -> a
forall a. Generic a => Rep a -> a
SOP.to (SOP I '[xs] -> a) -> (NP I xs -> SOP I '[xs]) -> NP I xs -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS (NP I) '[xs] -> SOP I '[xs]
forall k (f :: k -> Type) (xss :: [[k]]).
NS (NP f) xss -> SOP f xss
SOP (NS (NP I) '[xs] -> SOP I '[xs])
-> (NP I xs -> NS (NP I) '[xs]) -> NP I xs -> SOP I '[xs]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP I xs -> NS (NP I) '[xs]
forall k (a :: k -> Type) (x :: k) (xs :: [k]).
a x -> NS a (x : xs)
Z (NP I xs -> a) -> NP I xs -> a
forall a b. (a -> b) -> a -> b
$ Proxy LowerBound -> (forall a. LowerBound a => I a) -> NP I xs
forall k l (h :: (k -> Type) -> l -> Type) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> Type) (f :: k -> Type).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
SOP.hcpure (Proxy LowerBound
forall k (t :: k). Proxy t
Proxy @LowerBound) (a -> I a
forall a. a -> I a
I a
forall a. LowerBound a => a
lowerBound)