{-# 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 #-}
module Data.Record.Generic.SOP (
Field(..)
, fromSOP
, toSOP
, toDictAll
, 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)
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)
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
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)