{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}
-- | This is an internal module and subject to change. Should not be used in production

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(..))


-- | Helper functions to supply the datatype-info
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)






-- helper optics
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