{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Strongweak.Generic.Strengthen where
import Strongweak.Strengthen
import Data.Either.Validation
import GHC.Generics
import Data.Kind
import GHC.TypeNats
import GHC.Exts ( proxy#, Proxy# )
import Control.Applicative ( liftA2 )
strengthenGeneric
:: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s))
=> w -> Result s
strengthenGeneric :: forall w s.
(Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) =>
w -> Result s
strengthenGeneric = (Rep s Any -> s)
-> Validation Fails (Rep s Any) -> Validation Fails s
forall a b. (a -> b) -> Validation Fails a -> Validation Fails b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep s Any -> s
forall a x. Generic a => Rep a x -> a
forall x. Rep s x -> s
to (Validation Fails (Rep s Any) -> Validation Fails s)
-> (w -> Validation Fails (Rep s Any)) -> w -> Validation Fails s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep w Any -> Validation Fails (Rep s Any)
forall p. Rep w p -> Result (Rep s p)
forall {k} (w :: k -> Type) (s :: k -> Type) (p :: k).
GStrengthenD w s =>
w p -> Result (s p)
gstrengthenD (Rep w Any -> Validation Fails (Rep s Any))
-> (w -> Rep w Any) -> w -> Validation Fails (Rep s Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. w -> Rep w Any
forall x. w -> Rep w x
forall a x. Generic a => a -> Rep a x
from
class GStrengthenD w s where
gstrengthenD :: w p -> Result (s p)
instance GStrengthenC wcd scd w s => GStrengthenD (D1 wcd w) (D1 scd s) where
gstrengthenD :: forall (p :: k). D1 wcd w p -> Result (D1 scd s p)
gstrengthenD = (s p -> D1 scd s p)
-> Validation Fails (s p) -> Validation Fails (D1 scd s p)
forall a b. (a -> b) -> Validation Fails a -> Validation Fails b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap s p -> D1 scd s p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Validation Fails (s p) -> Validation Fails (D1 scd s p))
-> (D1 wcd w p -> Validation Fails (s p))
-> D1 wcd w p
-> Validation Fails (D1 scd s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {k} {k} (wcd :: k) (scd :: k) (w :: k -> Type)
(s :: k -> Type) (p :: k).
GStrengthenC wcd scd w s =>
w p -> Result (s p)
forall (wcd :: Meta) (scd :: Meta) (w :: k -> Type)
(s :: k -> Type) (p :: k).
GStrengthenC wcd scd w s =>
w p -> Result (s p)
gstrengthenC @wcd @scd (w p -> Validation Fails (s p))
-> (D1 wcd w p -> w p) -> D1 wcd w p -> Validation Fails (s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. D1 wcd w p -> w p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1
class GStrengthenC wcd scd w s where
gstrengthenC :: w p -> Result (s p)
instance GStrengthenC wcd scd V1 V1 where gstrengthenC :: forall (p :: k). V1 p -> Result (V1 p)
gstrengthenC = V1 p -> Validation Fails (V1 p)
forall e a. a -> Validation e a
Success
instance
( GStrengthenC wcd scd wl sl
, GStrengthenC wcd scd wr sr
) => GStrengthenC wcd scd (wl :+: wr) (sl :+: sr) where
gstrengthenC :: forall (p :: k). (:+:) wl wr p -> Result ((:+:) sl sr p)
gstrengthenC = \case L1 wl p
l -> sl p -> (:+:) sl sr p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (sl p -> (:+:) sl sr p)
-> Validation Fails (sl p) -> Result ((:+:) sl sr p)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (wcd :: k) (scd :: k) (w :: k -> Type) (s :: k -> Type)
(p :: k).
GStrengthenC wcd scd w s =>
w p -> Result (s p)
forall {k} {k} {k} (wcd :: k) (scd :: k) (w :: k -> Type)
(s :: k -> Type) (p :: k).
GStrengthenC wcd scd w s =>
w p -> Result (s p)
gstrengthenC @wcd @scd wl p
l
R1 wr p
r -> sr p -> (:+:) sl sr p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (sr p -> (:+:) sl sr p)
-> Validation Fails (sr p) -> Result ((:+:) sl sr p)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (wcd :: k) (scd :: k) (w :: k -> Type) (s :: k -> Type)
(p :: k).
GStrengthenC wcd scd w s =>
w p -> Result (s p)
forall {k} {k} {k} (wcd :: k) (scd :: k) (w :: k -> Type)
(s :: k -> Type) (p :: k).
GStrengthenC wcd scd w s =>
w p -> Result (s p)
gstrengthenC @wcd @scd wr p
r
instance GStrengthenS wcd scd wcc scc 0 w s
=> GStrengthenC wcd scd (C1 wcc w) (C1 scc s) where
gstrengthenC :: forall (p :: k). C1 wcc w p -> Result (C1 scc s p)
gstrengthenC = (s p -> C1 scc s p)
-> Validation Fails (s p) -> Validation Fails (C1 scc s p)
forall a b. (a -> b) -> Validation Fails a -> Validation Fails b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap s p -> C1 scc s p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Validation Fails (s p) -> Validation Fails (C1 scc s p))
-> (C1 wcc w p -> Validation Fails (s p))
-> C1 wcc w p
-> Validation Fails (C1 scc s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (wcd :: k) (scd :: k) (wcc :: Meta) (scc :: Meta)
(si :: Natural) (w :: k -> Type) (s :: k -> Type) (p :: k).
GStrengthenS wcd scd wcc scc si w s =>
w p -> Result (s p)
forall {k} {k} {k} {k} {k} (wcd :: k) (scd :: k) (wcc :: k)
(scc :: k) (si :: Natural) (w :: k -> Type) (s :: k -> Type)
(p :: k).
GStrengthenS wcd scd wcc scc si w s =>
w p -> Result (s p)
gstrengthenS @wcd @scd @wcc @scc @0 (w p -> Validation Fails (s p))
-> (C1 wcc w p -> w p) -> C1 wcc w p -> Validation Fails (s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C1 wcc w p -> w p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1
class GStrengthenS wcd scd wcc scc (si :: Natural) w s where
gstrengthenS :: w p -> Result (s p)
instance GStrengthenS wcd scd wcc scc si U1 U1 where gstrengthenS :: forall (p :: k). U1 p -> Result (U1 p)
gstrengthenS = U1 p -> Validation Fails (U1 p)
forall e a. a -> Validation e a
Success
instance
( GStrengthenS wcd scd wcc scc si wl sl
, GStrengthenS wcd scd wcc scc (si + ProdArity wl) wr sr
) => GStrengthenS wcd scd wcc scc si (wl :*: wr) (sl :*: sr) where
gstrengthenS :: forall p. (:*:) wl wr p -> Result ((:*:) sl sr p)
gstrengthenS (wl p
l :*: wr p
r) =
(sl p -> sr p -> (:*:) sl sr p)
-> Validation Fails (sl p)
-> Validation Fails (sr p)
-> Validation Fails ((:*:) sl sr p)
forall a b c.
(a -> b -> c)
-> Validation Fails a -> Validation Fails b -> Validation Fails c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 sl p -> sr p -> (:*:) sl sr p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
(:*:)
(forall (wcd :: k) (scd :: k) (wcc :: k) (scc :: k) (si :: Natural)
(w :: Type -> Type) (s :: Type -> Type) p.
GStrengthenS wcd scd wcc scc si w s =>
w p -> Result (s p)
forall {k} {k} {k} {k} {k} (wcd :: k) (scd :: k) (wcc :: k)
(scc :: k) (si :: Natural) (w :: k -> Type) (s :: k -> Type)
(p :: k).
GStrengthenS wcd scd wcc scc si w s =>
w p -> Result (s p)
gstrengthenS @wcd @scd @wcc @scc @si wl p
l)
(forall (wcd :: k) (scd :: k) (wcc :: k) (scc :: k) (si :: Natural)
(w :: Type -> Type) (s :: Type -> Type) p.
GStrengthenS wcd scd wcc scc si w s =>
w p -> Result (s p)
forall {k} {k} {k} {k} {k} (wcd :: k) (scd :: k) (wcc :: k)
(scc :: k) (si :: Natural) (w :: k -> Type) (s :: k -> Type)
(p :: k).
GStrengthenS wcd scd wcc scc si w s =>
w p -> Result (s p)
gstrengthenS @wcd @scd @wcc @scc @(si + ProdArity wl) wr p
r)
instance GStrengthenS wcd scd wcc scc si (S1 wcs (Rec0 a)) (S1 scs (Rec0 a)) where
gstrengthenS :: forall (p :: k). S1 wcs (Rec0 a) p -> Result (S1 scs (Rec0 a) p)
gstrengthenS = S1 scs (Rec0 a) p -> Validation Fails (S1 scs (Rec0 a) p)
forall e a. a -> Validation e a
Success (S1 scs (Rec0 a) p -> Validation Fails (S1 scs (Rec0 a) p))
-> (S1 wcs (Rec0 a) p -> S1 scs (Rec0 a) p)
-> S1 wcs (Rec0 a) p
-> Validation Fails (S1 scs (Rec0 a) p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec0 a p -> S1 scs (Rec0 a) p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Rec0 a p -> S1 scs (Rec0 a) p)
-> (S1 wcs (Rec0 a) p -> Rec0 a p)
-> S1 wcs (Rec0 a) p
-> S1 scs (Rec0 a) p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. S1 wcs (Rec0 a) p -> Rec0 a p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1
instance {-# OVERLAPS #-}
( Weak s ~ w
, Strengthen s
, Datatype wcd, Datatype scd
, Constructor wcc, Constructor scc
, Selector wcs, Selector scs
, KnownNat si
) => GStrengthenS wcd scd wcc scc si (S1 wcs (Rec0 w)) (S1 scs (Rec0 s)) where
gstrengthenS :: forall (p :: k). S1 wcs (Rec0 w) p -> Result (S1 scs (Rec0 s) p)
gstrengthenS = M1 S wcs (Rec0 w) p -> Rec0 w p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1 (M1 S wcs (Rec0 w) p -> Rec0 w p)
-> (Rec0 w p -> w) -> M1 S wcs (Rec0 w) p -> w
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> Rec0 w p -> w
forall k i c (p :: k). K1 i c p -> c
unK1 (M1 S wcs (Rec0 w) p -> w)
-> (w -> Result s) -> M1 S wcs (Rec0 w) p -> Result s
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> w -> Result s
Weak s -> Result s
forall a. Strengthen a => Weak a -> Result a
strengthen (M1 S wcs (Rec0 w) p -> Result s)
-> (Result s -> Result (S1 scs (Rec0 s) p))
-> M1 S wcs (Rec0 w) p
-> Result (S1 scs (Rec0 s) p)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> \case
Success s
s -> S1 scs (Rec0 s) p -> Result (S1 scs (Rec0 s) p)
forall e a. a -> Validation e a
Success (S1 scs (Rec0 s) p -> Result (S1 scs (Rec0 s) p))
-> S1 scs (Rec0 s) p -> Result (S1 scs (Rec0 s) p)
forall a b. (a -> b) -> a -> b
$ Rec0 s p -> S1 scs (Rec0 s) p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (Rec0 s p -> S1 scs (Rec0 s) p) -> Rec0 s p -> S1 scs (Rec0 s) p
forall a b. (a -> b) -> a -> b
$ s -> Rec0 s p
forall k i c (p :: k). c -> K1 i c p
K1 s
s
Failure Fails
es -> Fails -> Result (S1 scs (Rec0 s) p)
forall e a. e -> Validation e a
Failure (Fails -> Result (S1 scs (Rec0 s) p))
-> Fails -> Result (S1 scs (Rec0 s) p)
forall a b. (a -> b) -> a -> b
$ Fail -> Fails
forall a. a -> NeAcc a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Fail
e
where
e :: Fail
e = String
-> String
-> String
-> String
-> Natural
-> Maybe String
-> Natural
-> Maybe String
-> Fails
-> Fail
FailField String
wcd String
scd String
wcc String
scc Natural
si Maybe String
wcs Natural
si Maybe String
scs Fails
es
wcd :: String
wcd = forall (d :: k). Datatype d => String
forall {k} (d :: k). Datatype d => String
datatypeName' @wcd
scd :: String
scd = forall (d :: k). Datatype d => String
forall {k} (d :: k). Datatype d => String
datatypeName' @scd
wcc :: String
wcc = forall (c :: k). Constructor c => String
forall {k} (c :: k). Constructor c => String
conName' @wcc
scc :: String
scc = forall (c :: k). Constructor c => String
forall {k} (c :: k). Constructor c => String
conName' @scc
wcs :: Maybe String
wcs = forall {k} (s :: k). Selector s => Maybe String
forall (s :: Meta). Selector s => Maybe String
selName'' @wcs
scs :: Maybe String
scs = forall {k} (s :: k). Selector s => Maybe String
forall (s :: Meta). Selector s => Maybe String
selName'' @scs
si :: Natural
si = forall (n :: Natural). KnownNat n => Natural
natVal'' @si
(.>) :: (a -> b) -> (b -> c) -> a -> c
a -> b
f .> :: forall a b c. (a -> b) -> (b -> c) -> a -> c
.> b -> c
g = b -> c
g (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f
selName'' :: forall s. Selector s => Maybe String
selName'' :: forall {k} (s :: k). Selector s => Maybe String
selName'' = case forall (s :: k). Selector s => String
forall {k} (s :: k). Selector s => String
selName' @s of String
"" -> Maybe String
forall a. Maybe a
Nothing
String
s -> String -> Maybe String
forall a. a -> Maybe a
Just String
s
conName' :: forall c. Constructor c => String
conName' :: forall {k} (c :: k). Constructor c => String
conName' = forall (c :: k) k1 (t :: k -> (k1 -> Type) -> k1 -> Type)
(f :: k1 -> Type) (a :: k1).
Constructor c =>
t c f a -> String
forall {k} (c :: k) k1 (t :: k -> (k1 -> Type) -> k1 -> Type)
(f :: k1 -> Type) (a :: k1).
Constructor c =>
t c f a -> String
conName @c Any c Any Any
forall a. HasCallStack => a
undefined
datatypeName' :: forall d. Datatype d => String
datatypeName' :: forall {k} (d :: k). Datatype d => String
datatypeName' = forall (d :: k) k1 (t :: k -> (k1 -> Type) -> k1 -> Type)
(f :: k1 -> Type) (a :: k1).
Datatype d =>
t d f a -> String
forall {k} (d :: k) k1 (t :: k -> (k1 -> Type) -> k1 -> Type)
(f :: k1 -> Type) (a :: k1).
Datatype d =>
t d f a -> String
datatypeName @d Any d Any Any
forall a. HasCallStack => a
undefined
selName' :: forall s. Selector s => String
selName' :: forall {k} (s :: k). Selector s => String
selName' = forall (s :: k) k1 (t :: k -> (k1 -> Type) -> k1 -> Type)
(f :: k1 -> Type) (a :: k1).
Selector s =>
t s f a -> String
forall {k} (s :: k) k1 (t :: k -> (k1 -> Type) -> k1 -> Type)
(f :: k1 -> Type) (a :: k1).
Selector s =>
t s f a -> String
selName @s Any s Any Any
forall a. HasCallStack => a
undefined
type family ProdArity (f :: Type -> Type) :: Natural where
ProdArity (S1 c f) = 1
ProdArity (l :*: r) = ProdArity l + ProdArity r
natVal'' :: forall n. KnownNat n => Natural
natVal'' :: forall (n :: Natural). KnownNat n => Natural
natVal'' = Proxy# n -> Natural
forall (n :: Natural). KnownNat n => Proxy# n -> Natural
natVal' (Proxy# n
forall {k} (a :: k). Proxy# a
proxy# :: Proxy# n)
{-# INLINE natVal'' #-}