{-# language DataKinds #-} {-# language FlexibleContexts #-} {-# language FlexibleInstances #-} {-# language GADTs #-} {-# language MultiParamTypeClasses #-} {-# language PartialTypeSignatures #-} {-# language PolyKinds #-} {-# language QuantifiedConstraints #-} {-# language ScopedTypeVariables #-} {-# language TypeApplications #-} {-# language TypeFamilies #-} {-# language TypeOperators #-} {-# language UndecidableInstances #-} module Generics.Kind.Derive.Json where import Control.Applicative import Control.Monad import Data.Aeson import Data.Aeson.Types import Data.Kind import Data.Proxy import GHC.Generics (Meta (..)) import GHC.TypeLits import Generics.Kind gtoJSON' :: forall t. (GenericK t, GToJSONK (RepK t) 'LoT0) => t -> Value gtoJSON' :: forall t. (GenericK @(*) t, GToJSONK @(*) (RepK @(*) t) 'LoT0) => t -> Value gtoJSON' t x = RepK @(*) t 'LoT0 -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON (forall k (f :: k) (x :: LoT k). GenericK @k f => (:@@:) @k f x -> RepK @k f x fromK @_ @t @'LoT0 t (:@@:) @(*) t 'LoT0 x) gfromJSON' :: forall t. (GenericK t, GFromJSONK (RepK t) 'LoT0) => Value -> Parser t gfromJSON' :: forall t. (GenericK @(*) t, GFromJSONK @(*) (RepK @(*) t) 'LoT0) => Value -> Parser t gfromJSON' Value v = (RepK @(*) t 'LoT0 -> t) -> Parser (RepK @(*) t 'LoT0) -> Parser t forall a b. (a -> b) -> Parser a -> Parser b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (forall k (f :: k) (x :: LoT k). GenericK @k f => RepK @k f x -> (:@@:) @k f x toK @_ @t @'LoT0) (Value -> Parser (RepK @(*) t 'LoT0) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON Value v) class GToJSONK (f :: LoT k -> Type) (x :: LoT k) where gtoJSON :: f x -> Value class GFromJSONK (f :: LoT k -> Type) (x :: LoT k) where gfromJSON :: Value -> Parser (f x) instance ToJSON (Interpret t x) => GToJSONK (Field t) x where gtoJSON :: Field @k t x -> Value gtoJSON (Field Interpret @k @(*) t x t) = Interpret @k @(*) t x -> Value forall a. ToJSON a => a -> Value toJSON Interpret @k @(*) t x t instance FromJSON (Interpret t x) => GFromJSONK (Field t) x where gfromJSON :: Value -> Parser (Field @k t x) gfromJSON = (Interpret @k @(*) t x -> Field @k t x) -> Parser (Interpret @k @(*) t x) -> Parser (Field @k t x) forall a b. (a -> b) -> Parser a -> Parser b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Interpret @k @(*) t x -> Field @k t x forall {d} (t :: Atom @LiftedRep d (*)) (x :: LoT d). Interpret @d @(*) t x -> Field @d t x Field (Parser (Interpret @k @(*) t x) -> Parser (Field @k t x)) -> (Value -> Parser (Interpret @k @(*) t x)) -> Value -> Parser (Field @k t x) forall b c a. (b -> c) -> (a -> b) -> a -> c . Value -> Parser (Interpret @k @(*) t x) forall a. FromJSON a => Value -> Parser a parseJSON instance GToJSONK U1 x where gtoJSON :: U1 @(LoT k) x -> Value gtoJSON U1 @(LoT k) x U1 = Value Null instance GFromJSONK U1 x where gfromJSON :: Value -> Parser (U1 @(LoT k) x) gfromJSON Value Null = U1 @(LoT k) x -> Parser (U1 @(LoT k) x) forall a. a -> Parser a forall (f :: * -> *) a. Applicative f => a -> f a pure U1 @(LoT k) x forall k (p :: k). U1 @k p U1 gfromJSON Value _ = Parser (U1 @(LoT k) x) forall a. Parser a forall (f :: * -> *) a. Alternative f => f a empty instance (GToJSONK f x, GToJSONK g x) => GToJSONK (f :+: g) x where gtoJSON :: (:+:) @(LoT k) f g x -> Value gtoJSON (L1 f x f) = f x -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON f x f gtoJSON (R1 g x g) = g x -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON g x g instance (GFromJSONK f x, GFromJSONK g x) => GFromJSONK (f :+: g) x where gfromJSON :: Value -> Parser ((:+:) @(LoT k) f g x) gfromJSON Value v = (f x -> (:+:) @(LoT k) f g x forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) @k f g p L1 (f x -> (:+:) @(LoT k) f g x) -> Parser (f x) -> Parser ((:+:) @(LoT k) f g x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Value -> Parser (f x) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON Value v) Parser ((:+:) @(LoT k) f g x) -> Parser ((:+:) @(LoT k) f g x) -> Parser ((:+:) @(LoT k) f g x) forall a. Parser a -> Parser a -> Parser a forall (f :: * -> *) a. Alternative f => f a -> f a -> f a <|> (g x -> (:+:) @(LoT k) f g x forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) @k f g p R1 (g x -> (:+:) @(LoT k) f g x) -> Parser (g x) -> Parser ((:+:) @(LoT k) f g x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Value -> Parser (g x) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON Value v) instance (GToJSONK f x, GToJSONK g x) => GToJSONK (f :*: g) x where gtoJSON :: (:*:) @(LoT k) f g x -> Value gtoJSON (f x f :*: g x g) = (Value, Value) -> Value forall a. ToJSON a => a -> Value toJSON (f x -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON f x f, g x -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON g x g) instance (GFromJSONK f x, GFromJSONK g x) => GFromJSONK (f :*: g) x where gfromJSON :: Value -> Parser ((:*:) @(LoT k) f g x) gfromJSON Value v = do (Value f, Value g) <- Value -> Parser (Value, Value) forall a. FromJSON a => Value -> Parser a parseJSON Value v f x -> g x -> (:*:) @(LoT k) f g x forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> g p -> (:*:) @k f g p (:*:) (f x -> g x -> (:*:) @(LoT k) f g x) -> Parser (f x) -> Parser (g x -> (:*:) @(LoT k) f g x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Value -> Parser (f x) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON Value f Parser (g x -> (:*:) @(LoT k) f g x) -> Parser (g x) -> Parser ((:*:) @(LoT k) f g x) forall a b. Parser (a -> b) -> Parser a -> Parser b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b <*> Value -> Parser (g x) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON Value g instance forall name f x i fx st. (GToJSONK f x, KnownSymbol name) => GToJSONK (M1 i ('MetaCons name fx st) f) x where gtoJSON :: M1 @(LoT k) i ('MetaCons name fx st) f x -> Value gtoJSON (M1 f x f) = (String, Value) -> Value forall a. ToJSON a => a -> Value toJSON (Proxy @Symbol name -> String forall (n :: Symbol) (proxy :: Symbol -> *). KnownSymbol n => proxy n -> String symbolVal (Proxy @Symbol name -> String) -> Proxy @Symbol name -> String forall a b. (a -> b) -> a -> b $ forall {k} (t :: k). Proxy @k t forall (t :: Symbol). Proxy @Symbol t Proxy @name, f x -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON f x f) instance forall name f x i fx st. (GFromJSONK f x, KnownSymbol name) => GFromJSONK (M1 i ('MetaCons name fx st) f) x where gfromJSON :: Value -> Parser (M1 @(LoT k) i ('MetaCons name fx st) f x) gfromJSON Value v = do (String name, Value f) <- Value -> Parser (String, Value) forall a. FromJSON a => Value -> Parser a parseJSON Value v Bool -> Parser () forall (f :: * -> *). Alternative f => Bool -> f () guard (Bool -> Parser ()) -> Bool -> Parser () forall a b. (a -> b) -> a -> b $ String name String -> String -> Bool forall a. Eq a => a -> a -> Bool == Proxy @Symbol name -> String forall (n :: Symbol) (proxy :: Symbol -> *). KnownSymbol n => proxy n -> String symbolVal (forall {k} (t :: k). Proxy @k t forall (t :: Symbol). Proxy @Symbol t Proxy @name) f x -> M1 @(LoT k) i ('MetaCons name fx st) f x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 @k i c f p M1 (f x -> M1 @(LoT k) i ('MetaCons name fx st) f x) -> Parser (f x) -> Parser (M1 @(LoT k) i ('MetaCons name fx st) f x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Value -> Parser (f x) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON Value f instance GToJSONK f x => GToJSONK (M1 i ('MetaData _1 _2 _3 _4) f) x where gtoJSON :: M1 @(LoT k) i ('MetaData _1 _2 _3 _4) f x -> Value gtoJSON (M1 f x f) = f x -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON f x f instance GFromJSONK f x => GFromJSONK (M1 i ('MetaData _1 _2 _3 _4) f) x where gfromJSON :: Value -> Parser (M1 @(LoT k) i ('MetaData _1 _2 _3 _4) f x) gfromJSON = (f x -> M1 @(LoT k) i ('MetaData _1 _2 _3 _4) f x) -> Parser (f x) -> Parser (M1 @(LoT k) i ('MetaData _1 _2 _3 _4) f x) forall a b. (a -> b) -> Parser a -> Parser b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap f x -> M1 @(LoT k) i ('MetaData _1 _2 _3 _4) f x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 @k i c f p M1 (Parser (f x) -> Parser (M1 @(LoT k) i ('MetaData _1 _2 _3 _4) f x)) -> (Value -> Parser (f x)) -> Value -> Parser (M1 @(LoT k) i ('MetaData _1 _2 _3 _4) f x) forall b c a. (b -> c) -> (a -> b) -> a -> c . Value -> Parser (f x) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON instance GToJSONK f x => GToJSONK (M1 i ('MetaSel _1 _2 _3 _4) f) x where gtoJSON :: M1 @(LoT k) i ('MetaSel _1 _2 _3 _4) f x -> Value gtoJSON (M1 f x f) = f x -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON f x f instance GFromJSONK f x => GFromJSONK (M1 i ('MetaSel _1 _2 _3 _4) f) x where gfromJSON :: Value -> Parser (M1 @(LoT k) i ('MetaSel _1 _2 _3 _4) f x) gfromJSON = (f x -> M1 @(LoT k) i ('MetaSel _1 _2 _3 _4) f x) -> Parser (f x) -> Parser (M1 @(LoT k) i ('MetaSel _1 _2 _3 _4) f x) forall a b. (a -> b) -> Parser a -> Parser b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap f x -> M1 @(LoT k) i ('MetaSel _1 _2 _3 _4) f x forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 @k i c f p M1 (Parser (f x) -> Parser (M1 @(LoT k) i ('MetaSel _1 _2 _3 _4) f x)) -> (Value -> Parser (f x)) -> Value -> Parser (M1 @(LoT k) i ('MetaSel _1 _2 _3 _4) f x) forall b c a. (b -> c) -> (a -> b) -> a -> c . Value -> Parser (f x) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON instance (Interpret c x => GToJSONK f x) => GToJSONK (c :=>: f) x where gtoJSON :: (:=>:) @k c f x -> Value gtoJSON (SuchThat f x f) = f x -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON f x f instance (Interpret c x, GFromJSONK f x) => GFromJSONK (c :=>: f) x where gfromJSON :: Value -> Parser ((:=>:) @k c f x) gfromJSON = (f x -> (:=>:) @k c f x) -> Parser (f x) -> Parser ((:=>:) @k c f x) forall a b. (a -> b) -> Parser a -> Parser b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap f x -> (:=>:) @k c f x forall {d} (c :: Atom @LiftedRep d Constraint) (x :: LoT d) (f :: LoT d -> *). Interpret @d @Constraint c x => f x -> (:=>:) @d c f x SuchThat (Parser (f x) -> Parser ((:=>:) @k c f x)) -> (Value -> Parser (f x)) -> Value -> Parser ((:=>:) @k c f x) forall b c a. (b -> c) -> (a -> b) -> a -> c . Value -> Parser (f x) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON instance (forall t. GToJSONK f (t ':&&: x)) => GToJSONK (Exists k f) x where gtoJSON :: Exists @k k f x -> Value gtoJSON (Exists f ((':&&:) @k @k t x) x) = f ((':&&:) @k @k t x) -> Value forall k (f :: LoT k -> *) (x :: LoT k). GToJSONK @k f x => f x -> Value gtoJSON f ((':&&:) @k @k t x) x instance (forall t. GFromJSONK f (t ':&&: x)) => GFromJSONK (Exists k f) x where gfromJSON :: Value -> Parser (Exists @k k f x) gfromJSON = (f ((':&&:) @k @k (Any @k) x) -> Exists @k k f x) -> Parser (f ((':&&:) @k @k (Any @k) x)) -> Parser (Exists @k k f x) forall a b. (a -> b) -> Parser a -> Parser b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap f ((':&&:) @k @k (Any @k) x) -> Exists @k k f x forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d). f ((':&&:) @k @d t x) -> Exists @d k f x Exists (Parser (f ((':&&:) @k @k (Any @k) x)) -> Parser (Exists @k k f x)) -> (Value -> Parser (f ((':&&:) @k @k (Any @k) x))) -> Value -> Parser (Exists @k k f x) forall b c a. (b -> c) -> (a -> b) -> a -> c . Value -> Parser (f ((':&&:) @k @k (Any @k) x)) forall k (f :: LoT k -> *) (x :: LoT k). GFromJSONK @k f x => Value -> Parser (f x) gfromJSON