{-# 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 TypeOperators           #-}
{-# 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.Foldable (toList)
import Data.Kind
import Data.Primitive.SmallArray
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 Generics.SOP as SOP

import Data.Record.Generic
import Data.Record.Generic.LowerBound hiding (glowerBound)
import Data.Record.Generic.Rep.Internal (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 :: forall a (f :: * -> *).
SListI (MetadataOf a) =>
NP (Field f) (MetadataOf a) -> Rep f a
fromSOP =
    forall (f :: * -> *) a. SmallArray (f Any) -> Rep f a
Rep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> SmallArray a
smallArrayFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
SOP.hcollapse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
SOP.hmap forall (f :: * -> *) (field :: (Symbol, *)).
Field f field -> K (f Any) field
conv
  where
    conv :: Field f field -> K (f Any) field
    conv :: forall (f :: * -> *) (field :: (Symbol, *)).
Field f field -> K (f Any) field
conv (Field f (FieldType field)
fx) = forall k a (b :: k). a -> K a b
K forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
noInlineUnsafeCo f (FieldType field)
fx

toSOP :: SListI (MetadataOf a) => Rep f a -> Maybe (NP (Field f) (MetadataOf a))
toSOP :: forall a (f :: * -> *).
SListI (MetadataOf a) =>
Rep f a -> Maybe (NP (Field f) (MetadataOf a))
toSOP (Rep SmallArray (f Any)
v) =
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
SOP.hmap forall (f :: * -> *) (field :: (Symbol, *)).
K (f Any) field -> Field f field
conv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (xs :: [k]) a. SListI xs => [a] -> Maybe (NP (K a) xs)
SOP.fromList (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList SmallArray (f Any)
v)
  where
    conv :: K (f Any) field -> Field f field
    conv :: forall (f :: * -> *) (field :: (Symbol, *)).
K (f Any) field -> Field f field
conv (K f Any
fx) = forall (f :: * -> *) (field :: (Symbol, *)).
f (FieldType field) -> Field f field
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 :: forall (f :: * -> *) a (c :: * -> Constraint).
(Generic a, Constraints a (Compose c f),
 All IsField (MetadataOf a),
 forall (nm :: Symbol) 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
_ =
    case forall a (f :: * -> *).
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 -> forall a. HasCallStack => String -> a
error String
"toDictAll: invalid dictionary"
      Just NP (Field (Dict (Compose c f))) (MetadataOf a)
d  -> forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP (forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(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 (forall {k} (t :: k). Proxy t
Proxy @IsField) forall (field :: (Symbol, *)).
IsField field =>
Field (Dict (Compose c f)) field
-> Dict (Compose c (Field f)) field
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 = forall a (c :: * -> Constraint).
(Generic a, Constraints a c) =>
Proxy c -> Rep (Dict c) a
dict (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 :: forall (field :: (Symbol, *)).
IsField field =>
Field (Dict (Compose c f)) field
-> Dict (Compose c (Field f)) field
conv (Field Dict (Compose c f) (FieldType field)
Dict) = 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 :: forall a (xs :: [*]).
(Generic a, All LowerBound xs, Code a ~ '[xs]) =>
a
glowerBound = forall a. Generic a => Rep a -> a
SOP.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 a b. (a -> b) -> a -> b
$ forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
SOP.hcpure (forall {k} (t :: k). Proxy t
Proxy @LowerBound) (forall a. a -> I a
I forall a. LowerBound a => a
lowerBound)