{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Exinst.Aeson () where
import qualified Data.Aeson as Ae
import Data.Constraint
import Data.Kind (Type)
import Data.Singletons
import Exinst
import Prelude
instance forall k1 (f :: k1 -> Type)
. ( SingKind k1
, Ae.ToJSON (Demote k1)
, Dict1 Ae.ToJSON f
) => Ae.ToJSON (Some1 f)
where
{-# INLINABLE toJSON #-}
toJSON :: Some1 f -> Value
toJSON = \Some1 f
some1x -> forall k1 (f1 :: k1 -> *) r.
Some1 f1
-> (forall (a1 :: k1). SingI a1 => Sing a1 -> f1 a1 -> r) -> r
withSome1Sing Some1 f
some1x forall a b. (a -> b) -> a -> b
$ \Sing a1
sa1 (f a1
x :: f a1) ->
case forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 Sing a1
sa1 :: Dict (Ae.ToJSON (f a1)) of
Dict (ToJSON (f a1))
Dict -> forall a. ToJSON a => a -> Value
Ae.toJSON (forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1, f a1
x)
instance forall k2 k1 (f :: k2 -> k1 -> Type)
. ( SingKind k2
, SingKind k1
, Ae.ToJSON (Demote k2)
, Ae.ToJSON (Demote k1)
, Dict2 Ae.ToJSON f
) => Ae.ToJSON (Some2 f)
where
{-# INLINABLE toJSON #-}
toJSON :: Some2 f -> Value
toJSON = \Some2 f
some2x -> forall k2 k1 (f2 :: k2 -> k1 -> *) r.
Some2 f2
-> (forall (a2 :: k2) (a1 :: k1).
(SingI a2, SingI a1) =>
Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
-> r
withSome2Sing Some2 f
some2x forall a b. (a -> b) -> a -> b
$ \Sing a2
sa2 Sing a1
sa1 (f a2 a1
x :: f a2 a1) ->
case forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
(a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 Sing a2
sa2 Sing a1
sa1 :: Dict (Ae.ToJSON (f a2 a1)) of
Dict (ToJSON (f a2 a1))
Dict -> forall a. ToJSON a => a -> Value
Ae.toJSON ((forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1), f a2 a1
x)
instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
. ( SingKind k3
, SingKind k2
, SingKind k1
, Ae.ToJSON (Demote k3)
, Ae.ToJSON (Demote k2)
, Ae.ToJSON (Demote k1)
, Dict3 Ae.ToJSON f
) => Ae.ToJSON (Some3 f)
where
{-# INLINABLE toJSON #-}
toJSON :: Some3 f -> Value
toJSON = \Some3 f
some3x -> forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) r.
Some3 f3
-> (forall (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a3, SingI a2, SingI a1) =>
Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
-> r
withSome3Sing Some3 f
some3x forall a b. (a -> b) -> a -> b
$ \Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 (f a3 a2 a1
x :: f a3 a2 a1) ->
case forall k0 k3 k2 k1 (c :: k0 -> Constraint)
(f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 :: Dict (Ae.ToJSON (f a3 a2 a1)) of
Dict (ToJSON (f a3 a2 a1))
Dict -> forall a. ToJSON a => a -> Value
Ae.toJSON ((forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a3
sa3, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1), f a3 a2 a1
x)
instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
. ( SingKind k4
, SingKind k3
, SingKind k2
, SingKind k1
, Ae.ToJSON (Demote k4)
, Ae.ToJSON (Demote k3)
, Ae.ToJSON (Demote k2)
, Ae.ToJSON (Demote k1)
, Dict4 Ae.ToJSON f
) => Ae.ToJSON (Some4 f)
where
{-# INLINABLE toJSON #-}
toJSON :: Some4 f -> Value
toJSON = \Some4 f
some4x -> forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) r.
Some4 f4
-> (forall (a4 :: k4) (a3 :: k3) (a2 :: k2) (a1 :: k1).
(SingI a4, SingI a3, SingI a2, SingI a1) =>
Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
-> r
withSome4Sing Some4 f
some4x forall a b. (a -> b) -> a -> b
$ \Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 (f a4 a3 a2 a1
x :: f a4 a3 a2 a1) ->
case forall k0 k4 k3 k2 k1 (c :: k0 -> Constraint)
(f4 :: k4 -> k3 -> k2 -> k1 -> k0) (a4 :: k4) (a3 :: k3) (a2 :: k2)
(a1 :: k1).
Dict4 c f4 =>
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
dict4 Sing a4
sa4 Sing a3
sa3 Sing a2
sa2 Sing a1
sa1 :: Dict (Ae.ToJSON (f a4 a3 a2 a1)) of
Dict (ToJSON (f a4 a3 a2 a1))
Dict -> forall a. ToJSON a => a -> Value
Ae.toJSON ((forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a4
sa4, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a3
sa3, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a2
sa2, forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing a1
sa1), f a4 a3 a2 a1
x)
instance forall k1 (f :: k1 -> Type)
. ( SingKind k1
, Ae.FromJSON (Demote k1)
, Dict1 Ae.FromJSON f
) => Ae.FromJSON (Some1 f)
where
{-# INLINABLE parseJSON #-}
parseJSON :: Value -> Parser (Some1 f)
parseJSON = \Value
v -> do
(Demote k1
rsa1, Value
v') <- forall a. FromJSON a => Value -> Parser a
Ae.parseJSON Value
v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
rsa1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
case forall k0 k1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) (a1 :: k1).
Dict1 c f1 =>
Sing a1 -> Dict (c (f1 a1))
dict1 Sing a
sa1 :: Dict (Ae.FromJSON (f a1)) of
Dict (FromJSON (f a))
Dict -> do
f a
x :: f a1 <- forall a. FromJSON a => Value -> Parser a
Ae.parseJSON Value
v'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k1 (f1 :: k1 -> *) (a1 :: k1). Sing a1 -> f1 a1 -> Some1 f1
Some1 Sing a
sa1 f a
x)
instance forall k2 k1 (f :: k2 -> k1 -> Type)
. ( SingKind k2
, SingKind k1
, Ae.FromJSON (Demote k2)
, Ae.FromJSON (Demote k1)
, Dict2 Ae.FromJSON f
) => Ae.FromJSON (Some2 f)
where
{-# INLINABLE parseJSON #-}
parseJSON :: Value -> Parser (Some2 f)
parseJSON = \Value
v -> do
((Demote k2
rsa2, Demote k1
rsa1), Value
v') <- forall a. FromJSON a => Value -> Parser a
Ae.parseJSON Value
v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k2
rsa2 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa2 :: Sing (a2 :: k2)) ->
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
rsa1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
case forall k0 k2 k1 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0)
(a2 :: k2) (a1 :: k1).
Dict2 c f2 =>
Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
dict2 Sing a
sa2 Sing a
sa1 :: Dict (Ae.FromJSON (f a2 a1)) of
Dict (FromJSON (f a a))
Dict -> do
f a a
x :: f a2 a1 <- forall a. FromJSON a => Value -> Parser a
Ae.parseJSON Value
v'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k2 k1 (f2 :: k2 -> k1 -> *) (a2 :: k2) (a1 :: k1).
Sing a2 -> Sing a1 -> f2 a2 a1 -> Some2 f2
Some2 Sing a
sa2 Sing a
sa1 f a a
x)
instance forall k3 k2 k1 (f :: k3 -> k2 -> k1 -> Type)
. ( SingKind k3
, SingKind k2
, SingKind k1
, Ae.FromJSON (Demote k3)
, Ae.FromJSON (Demote k2)
, Ae.FromJSON (Demote k1)
, Dict3 Ae.FromJSON f
) => Ae.FromJSON (Some3 f)
where
{-# INLINABLE parseJSON #-}
parseJSON :: Value -> Parser (Some3 f)
parseJSON = \Value
v -> do
((Demote k3
rsa3, Demote k2
rsa2, Demote k1
rsa1), Value
v') <- forall a. FromJSON a => Value -> Parser a
Ae.parseJSON Value
v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k3
rsa3 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa3 :: Sing (a3 :: k3)) ->
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k2
rsa2 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa2 :: Sing (a2 :: k2)) ->
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
rsa1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
case forall k0 k3 k2 k1 (c :: k0 -> Constraint)
(f3 :: k3 -> k2 -> k1 -> k0) (a3 :: k3) (a2 :: k2) (a1 :: k1).
Dict3 c f3 =>
Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
dict3 Sing a
sa3 Sing a
sa2 Sing a
sa1 :: Dict (Ae.FromJSON (f a3 a2 a1)) of
Dict (FromJSON (f a a a))
Dict -> do
f a a a
x :: f a3 a2 a1 <- forall a. FromJSON a => Value -> Parser a
Ae.parseJSON Value
v'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k3 k2 k1 (f3 :: k3 -> k2 -> k1 -> *) (a3 :: k3) (a2 :: k2)
(a1 :: k1).
Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> Some3 f3
Some3 Sing a
sa3 Sing a
sa2 Sing a
sa1 f a a a
x)
instance forall k4 k3 k2 k1 (f :: k4 -> k3 -> k2 -> k1 -> Type)
. ( SingKind k4
, SingKind k3
, SingKind k2
, SingKind k1
, Ae.FromJSON (Demote k4)
, Ae.FromJSON (Demote k3)
, Ae.FromJSON (Demote k2)
, Ae.FromJSON (Demote k1)
, Dict4 Ae.FromJSON f
) => Ae.FromJSON (Some4 f)
where
{-# INLINABLE parseJSON #-}
parseJSON :: Value -> Parser (Some4 f)
parseJSON = \Value
v -> do
((Demote k4
rsa4, Demote k3
rsa3, Demote k2
rsa2, Demote k1
rsa1), Value
v') <- forall a. FromJSON a => Value -> Parser a
Ae.parseJSON Value
v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k4
rsa4 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa4 :: Sing (a4 :: k4)) ->
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k3
rsa3 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa3 :: Sing (a3 :: k3)) ->
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k2
rsa2 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa2 :: Sing (a2 :: k2)) ->
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote k1
rsa1 forall a b. (a -> b) -> a -> b
$ \(Sing a
sa1 :: Sing (a1 :: k1)) ->
case forall k0 k4 k3 k2 k1 (c :: k0 -> Constraint)
(f4 :: k4 -> k3 -> k2 -> k1 -> k0) (a4 :: k4) (a3 :: k3) (a2 :: k2)
(a1 :: k1).
Dict4 c f4 =>
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))
dict4 Sing a
sa4 Sing a
sa3 Sing a
sa2 Sing a
sa1 :: Dict (Ae.FromJSON (f a4 a3 a2 a1)) of
Dict (FromJSON (f a a a a))
Dict -> do
f a a a a
x :: f a4 a3 a2 a1 <- forall a. FromJSON a => Value -> Parser a
Ae.parseJSON Value
v'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k4 k3 k2 k1 (f4 :: k4 -> k3 -> k2 -> k1 -> *) (a4 :: k4)
(a3 :: k3) (a2 :: k2) (a1 :: k1).
Sing a4
-> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> Some4 f4
Some4 Sing a
sa4 Sing a
sa3 Sing a
sa2 Sing a
sa1 f a a a a
x)
instance (Ae.FromJSON (l a1), Ae.FromJSON (r a1)) => Ae.FromJSON (S1 l r a1)
instance (Ae.FromJSON (l a2 a1), Ae.FromJSON (r a2 a1)) => Ae.FromJSON (S2 l r a2 a1)
instance (Ae.FromJSON (l a3 a2 a1), Ae.FromJSON (r a3 a2 a1)) => Ae.FromJSON (S3 l r a3 a2 a1)
instance (Ae.FromJSON (l a4 a3 a2 a1), Ae.FromJSON (r a4 a3 a2 a1)) => Ae.FromJSON (S4 l r a4 a3 a2 a1)
instance (Ae.ToJSON (l a1), Ae.ToJSON (r a1)) => Ae.ToJSON (S1 l r a1)
instance (Ae.ToJSON (l a2 a1), Ae.ToJSON (r a2 a1)) => Ae.ToJSON (S2 l r a2 a1)
instance (Ae.ToJSON (l a3 a2 a1), Ae.ToJSON (r a3 a2 a1)) => Ae.ToJSON (S3 l r a3 a2 a1)
instance (Ae.ToJSON (l a4 a3 a2 a1), Ae.ToJSON (r a4 a3 a2 a1)) => Ae.ToJSON (S4 l r a4 a3 a2 a1)
instance (Ae.FromJSON (l a1), Ae.FromJSON (r a1)) => Ae.FromJSON (P1 l r a1)
instance (Ae.FromJSON (l a2 a1), Ae.FromJSON (r a2 a1)) => Ae.FromJSON (P2 l r a2 a1)
instance (Ae.FromJSON (l a3 a2 a1), Ae.FromJSON (r a3 a2 a1)) => Ae.FromJSON (P3 l r a3 a2 a1)
instance (Ae.FromJSON (l a4 a3 a2 a1), Ae.FromJSON (r a4 a3 a2 a1)) => Ae.FromJSON (P4 l r a4 a3 a2 a1)
instance (Ae.ToJSON (l a1), Ae.ToJSON (r a1)) => Ae.ToJSON (P1 l r a1)
instance (Ae.ToJSON (l a2 a1), Ae.ToJSON (r a2 a1)) => Ae.ToJSON (P2 l r a2 a1)
instance (Ae.ToJSON (l a3 a2 a1), Ae.ToJSON (r a3 a2 a1)) => Ae.ToJSON (P3 l r a3 a2 a1)
instance (Ae.ToJSON (l a4 a3 a2 a1), Ae.ToJSON (r a4 a3 a2 a1)) => Ae.ToJSON (P4 l r a4 a3 a2 a1)