{- | 'strengthen' over generic representations.

Strengthen failures are annotated with precise information describing where the
failure occurred: datatype name, constructor name, field index (and name if
present). To achieve this, we split the generic derivation into 3 classes, each
handling/"unwrapping" a different layer of the generic representation: datatype
(D), constructor (C) and selector (S).
-}

-- both required due to type class design
{-# 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 )

-- | Strengthen a value generically.
--
-- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for
-- the definition of compatibility in this context.
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

-- | Generic strengthening at the datatype level.
class GStrengthenD w s where
    gstrengthenD :: w p -> Result (s p)

-- | Enter a datatype, stripping its metadata wrapper.
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

-- | Generic strengthening at the constructor sum level.
class GStrengthenC wcd scd w s where
    gstrengthenC :: w p -> Result (s p)

-- | Nothing to do for empty datatypes.
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

-- | Strengthen sum types by casing and strengthening left or right.
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

-- | Enter a constructor, stripping its metadata wrapper.
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

-- | Generic strengthening at the constructor level.
class GStrengthenS wcd scd wcc scc (si :: Natural) w s where
    gstrengthenS :: w p -> Result (s p)

-- | Nothing to do for empty constructors.
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

-- | Strengthen product types by strengthening left and right.
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)

-- | Special case: if source and target types are equal, copy the value through.
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

-- | Strengthen a field using the existing 'Strengthen' instance.
instance {-# OVERLAPS #-}
  ( Weak s ~ w -- has to be here, else "illegal typesym family app in instance"
  , 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

--------------------------------------------------------------------------------

-- from flow
(.>) :: (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

--------------------------------------------------------------------------------

-- | Get the record name for a selector if present.
--
-- On the type level, a 'Maybe Symbol' is stored for record names. But the
-- reification is done using @fromMaybe ""@. So we have to inspect the resulting
-- string to determine whether the field uses record syntax or not. (Silly.)
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' without the value (only used as a proxy). Lets us push our
--   'undefined's into one place.
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' without the value (only used as a proxy). Lets us push our
--   'undefined's into one place.
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' without the value (only used as a proxy). Lets us push our
--   'undefined's into one place.
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'' #-}