{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}
module Control.Validation.Internal.SOP where
import Data.Proxy(Proxy(..))
import Generics.SOP(constructorName, hpure, hmap, hcmap, constructorInfo, datatypeName, unI, ConstructorInfo(..), SListI, SListI2, NP, HasDatatypeInfo(..), ConstructorName, FieldName, POP(..), K(..), DatatypeName, Generic(..), FieldInfo(..), Rep, NS(..), I(..), NP(..))
errMsgPOP :: forall e a e'. (HasDatatypeInfo a) => Proxy a -> (DatatypeName -> ConstructorName -> FieldName -> e -> e') -> POP (K (e -> e')) (Code a)
errMsgPOP :: Proxy a
-> (DatatypeName -> DatatypeName -> DatatypeName -> e -> e')
-> POP (K (e -> e')) (Code a)
errMsgPOP p :: Proxy a
p f :: DatatypeName -> DatatypeName -> DatatypeName -> e -> e'
f = (DatatypeName -> DatatypeName -> e -> e')
-> NP ConstructorInfo (Code a) -> POP (K (e -> e')) (Code a)
forall e a e'.
SListI2 (Code a) =>
(DatatypeName -> DatatypeName -> e -> e')
-> NP ConstructorInfo (Code a) -> POP (K (e -> e')) (Code a)
errMsgPOP' @e @a (DatatypeName -> DatatypeName -> DatatypeName -> e -> e'
f (DatatypeName -> DatatypeName -> DatatypeName -> e -> e')
-> DatatypeName -> DatatypeName -> DatatypeName -> e -> e'
forall a b. (a -> b) -> a -> b
$ DatatypeInfo (Code a) -> DatatypeName
forall (xss :: [[*]]). DatatypeInfo xss -> DatatypeName
datatypeName DatatypeInfo (Code a)
inf) (DatatypeInfo (Code a) -> NP ConstructorInfo (Code a)
forall (xss :: [[*]]). DatatypeInfo xss -> NP ConstructorInfo xss
constructorInfo DatatypeInfo (Code a)
inf :: NP ConstructorInfo (Code a))
where inf :: DatatypeInfo (Code a)
inf = Proxy a -> DatatypeInfo (Code a)
forall a (proxy :: * -> *).
HasDatatypeInfo a =>
proxy a -> DatatypeInfo (Code a)
datatypeInfo Proxy a
p
errMsgPOP' :: forall e a e'. (SListI2 (Code a)) => (ConstructorName -> FieldName -> e -> e') -> NP ConstructorInfo (Code a) -> POP (K (e -> e')) (Code a)
errMsgPOP' :: (DatatypeName -> DatatypeName -> e -> e')
-> NP ConstructorInfo (Code a) -> POP (K (e -> e')) (Code a)
errMsgPOP' f :: DatatypeName -> DatatypeName -> e -> e'
f cinfos :: NP ConstructorInfo (Code a)
cinfos = NP (NP (K (e -> e'))) (Code a) -> POP (K (e -> e')) (Code a)
forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
POP (NP (NP (K (e -> e'))) (Code a) -> POP (K (e -> e')) (Code a))
-> NP (NP (K (e -> e'))) (Code a) -> POP (K (e -> e')) (Code a)
forall a b. (a -> b) -> a -> b
$ Proxy SListI
-> (forall (a :: [*]).
SListI a =>
ConstructorInfo a -> NP (K (e -> e')) a)
-> NP ConstructorInfo (Code a)
-> NP (NP (K (e -> e'))) (Code a)
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
hcmap (Proxy SListI
forall k (t :: k). Proxy t
Proxy @SListI) ((DatatypeName -> DatatypeName -> e -> e')
-> ConstructorInfo a -> NP (K (e -> e')) a
forall e (xs :: [*]) e'.
SListI xs =>
(DatatypeName -> DatatypeName -> e -> e')
-> ConstructorInfo xs -> NP (K (e -> e')) xs
errMsgNP DatatypeName -> DatatypeName -> e -> e'
f) NP ConstructorInfo (Code a)
cinfos
errMsgNP :: forall e xs e'. (SListI xs) => (ConstructorName -> FieldName -> e -> e') -> ConstructorInfo xs -> NP (K (e -> e')) xs
errMsgNP :: (DatatypeName -> DatatypeName -> e -> e')
-> ConstructorInfo xs -> NP (K (e -> e')) xs
errMsgNP f :: DatatypeName -> DatatypeName -> e -> e'
f = \case
Record name :: DatatypeName
name finfos :: NP FieldInfo xs
finfos -> (forall a. FieldInfo a -> K (e -> e') a)
-> NP FieldInfo xs -> NP (K (e -> e')) xs
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
hmap (\(FieldInfo fname) -> (e -> e') -> K (e -> e') a
forall k a (b :: k). a -> K a b
K ((e -> e') -> K (e -> e') a) -> (e -> e') -> K (e -> e') a
forall a b. (a -> b) -> a -> b
$ DatatypeName -> DatatypeName -> e -> e'
f DatatypeName
name DatatypeName
fname) NP FieldInfo xs
finfos
constr :: ConstructorInfo xs
constr -> (forall a. K (e -> e') a) -> NP (K (e -> e')) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure ((forall a. K (e -> e') a) -> NP (K (e -> e')) xs)
-> (forall a. K (e -> e') a) -> NP (K (e -> e')) xs
forall a b. (a -> b) -> a -> b
$ ((e -> e') -> K (e -> e') a
forall k a (b :: k). a -> K a b
K ((e -> e') -> K (e -> e') a) -> (e -> e') -> K (e -> e') a
forall a b. (a -> b) -> a -> b
$ DatatypeName -> DatatypeName -> e -> e'
f (ConstructorInfo xs -> DatatypeName
forall (xs :: [*]). ConstructorInfo xs -> DatatypeName
constructorName ConstructorInfo xs
constr) "" :: forall a. K (e -> e') a)
type Optic f s a = (a -> f a) -> (s -> f s)
type T' s a = forall f. Applicative f => Optic f s a
sopLensTo :: (Functor f, Generic a) => Optic f a (Rep a)
sopLensTo :: Optic f a (Rep a)
sopLensTo l :: Rep a -> f (Rep a)
l = (Rep a -> a) -> f (Rep a) -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep a -> a
forall a. Generic a => Rep a -> a
to (f (Rep a) -> f a) -> (a -> f (Rep a)) -> a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a -> f (Rep a)
l (Rep a -> f (Rep a)) -> (a -> Rep a) -> a -> f (Rep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a
forall a. Generic a => a -> Rep a
from
tZ :: T' (NS g (x ': xs)) (g x)
tZ :: Optic f (NS g (x : xs)) (g x)
tZ f :: g x -> f (g x)
f = \case
Z h :: g x
h -> g x -> NS g (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (g x -> NS g (x : xs)) -> f (g x) -> f (NS g (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g x -> f (g x)
f g x
g x
h
S t :: NS g xs
t -> NS g (x : xs) -> f (NS g (x : xs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NS g xs -> NS g (x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S NS g xs
t)
tS :: T' (NS g (x ': xs)) (NS g xs)
tS :: Optic f (NS g (x : xs)) (NS g xs)
tS f :: NS g xs -> f (NS g xs)
f = \case
Z h :: g x
h -> NS g (x : xs) -> f (NS g (x : xs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (g x -> NS g (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z g x
h)
S t :: NS g xs
t -> NS g xs -> NS g (x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S (NS g xs -> NS g (x : xs)) -> f (NS g xs) -> f (NS g (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NS g xs -> f (NS g xs)
f NS g xs
NS g xs
t
tI :: T' (I a) a
tI :: Optic f (I a) a
tI f :: a -> f a
f = (a -> I a) -> f a -> f (I a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> I a
forall a. a -> I a
I (f a -> f (I a)) -> (I a -> f a) -> I a -> f (I a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f a
f (a -> f a) -> (I a -> a) -> I a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. I a -> a
forall a. I a -> a
unI
tH :: T' (NP g (x ': xs)) (g x)
tH :: Optic f (NP g (x : xs)) (g x)
tH f :: g x -> f (g x)
f = \(x :: g x
x :* xs :: NP g xs
xs) -> (g x -> NP g xs -> NP g (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP g xs
xs) (g x -> NP g (x : xs)) -> f (g x) -> f (NP g (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g x -> f (g x)
f g x
g x
x
tT :: T' (NP g (x ': xs)) (NP g xs)
tT :: Optic f (NP g (x : xs)) (NP g xs)
tT f :: NP g xs -> f (NP g xs)
f = \(x :: g x
x :* xs :: NP g xs
xs) -> (g x
x g x -> NP g xs -> NP g (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:*) (NP g xs -> NP g (x : xs)) -> f (NP g xs) -> f (NP g (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NP g xs -> f (NP g xs)
f NP g xs
NP g xs
xs