{- | '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).
-}

{-# LANGUAGE AllowAmbiguousTypes #-}

module Strongweak.Generic.Strengthen where

import Strongweak.Strengthen
import Data.Either.Validation
import Data.List.NonEmpty
import GHC.Generics

import Numeric.Natural
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 -> Validation (NonEmpty StrengthenFail) s
strengthenGeneric :: forall w s.
(Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) =>
w -> Validation (NonEmpty StrengthenFail) s
strengthenGeneric = (Rep s Any -> s)
-> Validation (NonEmpty StrengthenFail) (Rep s Any)
-> Validation (NonEmpty StrengthenFail) s
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep s Any -> s
forall a x. Generic a => Rep a x -> a
to (Validation (NonEmpty StrengthenFail) (Rep s Any)
 -> Validation (NonEmpty StrengthenFail) s)
-> (w -> Validation (NonEmpty StrengthenFail) (Rep s Any))
-> w
-> Validation (NonEmpty StrengthenFail) s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep w Any -> Validation (NonEmpty StrengthenFail) (Rep s Any)
forall {k} (w :: k -> *) (s :: k -> *) (p :: k).
GStrengthenD w s =>
w p -> Validation (NonEmpty StrengthenFail) (s p)
gstrengthenD (Rep w Any -> Validation (NonEmpty StrengthenFail) (Rep s Any))
-> (w -> Rep w Any)
-> w
-> Validation (NonEmpty StrengthenFail) (Rep s Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. w -> Rep w Any
forall a x. Generic a => a -> Rep a x
from

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

-- | Enter a datatype, stripping its metadata wrapper.
instance (GStrengthenC w s, Datatype dw, Datatype ds) => GStrengthenD (D1 dw w) (D1 ds s) where
    gstrengthenD :: forall (p :: k).
D1 dw w p -> Validation (NonEmpty StrengthenFail) (D1 ds s p)
gstrengthenD = (s p -> D1 ds s p)
-> Validation (NonEmpty StrengthenFail) (s p)
-> Validation (NonEmpty StrengthenFail) (D1 ds s p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s p -> D1 ds s p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Validation (NonEmpty StrengthenFail) (s p)
 -> Validation (NonEmpty StrengthenFail) (D1 ds s p))
-> (D1 dw w p -> Validation (NonEmpty StrengthenFail) (s p))
-> D1 dw w p
-> Validation (NonEmpty StrengthenFail) (D1 ds s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> String -> w p -> Validation (NonEmpty StrengthenFail) (s p)
forall {k} (w :: k -> *) (s :: k -> *) (p :: k).
GStrengthenC w s =>
String
-> String -> w p -> Validation (NonEmpty StrengthenFail) (s p)
gstrengthenC (forall {k} (d :: k). Datatype d => String
forall (d :: Meta). Datatype d => String
datatypeName' @dw) (forall {k} (d :: k). Datatype d => String
forall (d :: Meta). Datatype d => String
datatypeName' @ds) (w p -> Validation (NonEmpty StrengthenFail) (s p))
-> (D1 dw w p -> w p)
-> D1 dw w p
-> Validation (NonEmpty StrengthenFail) (s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. D1 dw w p -> w p
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

-- | Generic strengthening at the constructor sum level.
class GStrengthenC w s where
    gstrengthenC :: String -> String -> w p -> Validation (NonEmpty StrengthenFail) (s p)

-- | Nothing to do for empty datatypes.
instance GStrengthenC V1 V1 where
    gstrengthenC :: forall (p :: k).
String
-> String -> V1 p -> Validation (NonEmpty StrengthenFail) (V1 p)
gstrengthenC String
_ String
_ = V1 p -> Validation (NonEmpty StrengthenFail) (V1 p)
forall e a. a -> Validation e a
Success

-- | Strengthen sum types by casing and strengthening left or right.
instance (GStrengthenC lw ls, GStrengthenC rw rs) => GStrengthenC (lw :+: rw) (ls :+: rs) where
    gstrengthenC :: forall (p :: k).
String
-> String
-> (:+:) lw rw p
-> Validation (NonEmpty StrengthenFail) ((:+:) ls rs p)
gstrengthenC String
dw String
ds = \case L1 lw p
l -> ls p -> (:+:) ls rs p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (ls p -> (:+:) ls rs p)
-> Validation (NonEmpty StrengthenFail) (ls p)
-> Validation (NonEmpty StrengthenFail) ((:+:) ls rs p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> String -> lw p -> Validation (NonEmpty StrengthenFail) (ls p)
forall {k} (w :: k -> *) (s :: k -> *) (p :: k).
GStrengthenC w s =>
String
-> String -> w p -> Validation (NonEmpty StrengthenFail) (s p)
gstrengthenC String
dw String
ds lw p
l
                               R1 rw p
r -> rs p -> (:+:) ls rs p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (rs p -> (:+:) ls rs p)
-> Validation (NonEmpty StrengthenFail) (rs p)
-> Validation (NonEmpty StrengthenFail) ((:+:) ls rs p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> String -> rw p -> Validation (NonEmpty StrengthenFail) (rs p)
forall {k} (w :: k -> *) (s :: k -> *) (p :: k).
GStrengthenC w s =>
String
-> String -> w p -> Validation (NonEmpty StrengthenFail) (s p)
gstrengthenC String
dw String
ds rw p
r

-- | Enter a constructor, stripping its metadata wrapper.
instance (GStrengthenS w s, Constructor cw, Constructor cs) => GStrengthenC (C1 cw w) (C1 cs s) where
    gstrengthenC :: forall (p :: k).
String
-> String
-> C1 cw w p
-> Validation (NonEmpty StrengthenFail) (C1 cs s p)
gstrengthenC String
dw String
ds = (s p -> C1 cs s p)
-> Validation (NonEmpty StrengthenFail) (s p)
-> Validation (NonEmpty StrengthenFail) (C1 cs s p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap s p -> C1 cs s p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Validation (NonEmpty StrengthenFail) (s p)
 -> Validation (NonEmpty StrengthenFail) (C1 cs s p))
-> (C1 cw w p -> Validation (NonEmpty StrengthenFail) (s p))
-> C1 cw w p
-> Validation (NonEmpty StrengthenFail) (C1 cs s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural, Validation (NonEmpty StrengthenFail) (s p))
-> Validation (NonEmpty StrengthenFail) (s p)
forall a b. (a, b) -> b
snd ((Natural, Validation (NonEmpty StrengthenFail) (s p))
 -> Validation (NonEmpty StrengthenFail) (s p))
-> (C1 cw w p
    -> (Natural, Validation (NonEmpty StrengthenFail) (s p)))
-> C1 cw w p
-> Validation (NonEmpty StrengthenFail) (s p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String
-> String
-> String
-> String
-> Natural
-> w p
-> (Natural, Validation (NonEmpty StrengthenFail) (s p))
forall {k} (w :: k -> *) (s :: k -> *) (p :: k).
GStrengthenS w s =>
String
-> String
-> String
-> String
-> Natural
-> w p
-> (Natural, Validation (NonEmpty StrengthenFail) (s p))
gstrengthenS String
dw String
ds (forall {k} (c :: k). Constructor c => String
forall (c :: Meta). Constructor c => String
conName' @cw) (forall {k} (c :: k). Constructor c => String
forall (c :: Meta). Constructor c => String
conName' @cs) Natural
0 (w p -> (Natural, Validation (NonEmpty StrengthenFail) (s p)))
-> (C1 cw w p -> w p)
-> C1 cw w p
-> (Natural, Validation (NonEmpty StrengthenFail) (s p))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. C1 cw w p -> w p
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

{- | Generic strengthening at the selector product level.

In order to calculate field indices, we return the current field index alongside
the result. This way, the product case can strengthen the left branch, then
increment the returned field index and use it for strengthening the right
branch.
-}
class GStrengthenS w s where
    gstrengthenS
        :: String  -- ^ weak   datatype name
        -> String  -- ^ strong datatype name
        -> String  -- ^ weak   constructor name
        -> String  -- ^ strong constructor name
        -> Natural -- ^ current field index (0, from left)
        -> w p -> (Natural, Validation (NonEmpty StrengthenFail) (s p))

-- | Nothing to do for empty constructors.
instance GStrengthenS U1 U1 where
    gstrengthenS :: forall (p :: k).
String
-> String
-> String
-> String
-> Natural
-> U1 p
-> (Natural, Validation (NonEmpty StrengthenFail) (U1 p))
gstrengthenS String
_ String
_ String
_ String
_ Natural
n U1 p
x = (Natural
n, U1 p -> Validation (NonEmpty StrengthenFail) (U1 p)
forall e a. a -> Validation e a
Success U1 p
x)

-- | Strengthen product types by strengthening left and right.
--
-- This is ordered (left then right) in order to pass the field index along.
instance (GStrengthenS lw ls, GStrengthenS rw rs) => GStrengthenS (lw :*: rw) (ls :*: rs) where
    gstrengthenS :: forall (p :: k).
String
-> String
-> String
-> String
-> Natural
-> (:*:) lw rw p
-> (Natural, Validation (NonEmpty StrengthenFail) ((:*:) ls rs p))
gstrengthenS String
dw String
ds String
cw String
cs Natural
n (lw p
l :*: rw p
r) = (Natural
n'', (ls p -> rs p -> (:*:) ls rs p)
-> Validation (NonEmpty StrengthenFail) (ls p)
-> Validation (NonEmpty StrengthenFail) (rs p)
-> Validation (NonEmpty StrengthenFail) ((:*:) ls rs p)
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ls p -> rs p -> (:*:) ls rs p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) Validation (NonEmpty StrengthenFail) (ls p)
l' Validation (NonEmpty StrengthenFail) (rs p)
r')
      where
        (Natural
n',  Validation (NonEmpty StrengthenFail) (ls p)
l') = String
-> String
-> String
-> String
-> Natural
-> lw p
-> (Natural, Validation (NonEmpty StrengthenFail) (ls p))
forall {k} (w :: k -> *) (s :: k -> *) (p :: k).
GStrengthenS w s =>
String
-> String
-> String
-> String
-> Natural
-> w p
-> (Natural, Validation (NonEmpty StrengthenFail) (s p))
gstrengthenS String
dw String
ds String
cw String
cs Natural
n      lw p
l
        (Natural
n'', Validation (NonEmpty StrengthenFail) (rs p)
r') = String
-> String
-> String
-> String
-> Natural
-> rw p
-> (Natural, Validation (NonEmpty StrengthenFail) (rs p))
forall {k} (w :: k -> *) (s :: k -> *) (p :: k).
GStrengthenS w s =>
String
-> String
-> String
-> String
-> Natural
-> w p
-> (Natural, Validation (NonEmpty StrengthenFail) (s p))
gstrengthenS String
dw String
ds String
cw String
cs (Natural
n'Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+Natural
1) rw p
r

-- | Special case: if source and target types are equal, copy the value through.
instance GStrengthenS (S1 mw (Rec0 w)) (S1 ms (Rec0 w)) where
    gstrengthenS :: forall (p :: k).
String
-> String
-> String
-> String
-> Natural
-> S1 mw (Rec0 w) p
-> (Natural,
    Validation (NonEmpty StrengthenFail) (S1 ms (Rec0 w) p))
gstrengthenS String
_ String
_ String
_ String
_ Natural
n S1 mw (Rec0 w) p
x = (Natural
n, S1 ms (Rec0 w) p
-> Validation (NonEmpty StrengthenFail) (S1 ms (Rec0 w) p)
forall e a. a -> Validation e a
Success (Rec0 w p -> S1 ms (Rec0 w) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (S1 mw (Rec0 w) p -> Rec0 w p
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1 S1 mw (Rec0 w) p
x)))

-- | Strengthen a field using the existing 'Strengthen' instance.
instance {-# OVERLAPS #-} (Strengthen s, Weak s ~ w, Selector mw, Selector ms) => GStrengthenS (S1 mw (Rec0 w)) (S1 ms (Rec0 s)) where
    gstrengthenS :: forall (p :: k).
String
-> String
-> String
-> String
-> Natural
-> S1 mw (Rec0 w) p
-> (Natural,
    Validation (NonEmpty StrengthenFail) (S1 ms (Rec0 s) p))
gstrengthenS String
dw String
ds String
cw String
cs Natural
n (M1 (K1 w
w)) =
        case Weak s -> Validation (NonEmpty StrengthenFail) s
forall a.
Strengthen a =>
Weak a -> Validation (NonEmpty StrengthenFail) a
strengthen w
Weak s
w of
          Failure NonEmpty StrengthenFail
es ->
            let fw :: Maybe String
fw = forall {k} (s :: k). Selector s => Maybe String
forall (s :: Meta). Selector s => Maybe String
selName'' @mw
                fs :: Maybe String
fs = forall {k} (s :: k). Selector s => Maybe String
forall (s :: Meta). Selector s => Maybe String
selName'' @ms
                e :: StrengthenFail
e  = String
-> String
-> String
-> String
-> Natural
-> Maybe String
-> Natural
-> Maybe String
-> NonEmpty StrengthenFail
-> StrengthenFail
StrengthenFailField String
dw String
ds String
cw String
cs Natural
n Maybe String
fw Natural
n Maybe String
fs NonEmpty StrengthenFail
es
            in  (Natural
n, NonEmpty StrengthenFail
-> Validation (NonEmpty StrengthenFail) (S1 ms (Rec0 s) p)
forall e a. e -> Validation e a
Failure (NonEmpty StrengthenFail
 -> Validation (NonEmpty StrengthenFail) (S1 ms (Rec0 s) p))
-> NonEmpty StrengthenFail
-> Validation (NonEmpty StrengthenFail) (S1 ms (Rec0 s) p)
forall a b. (a -> b) -> a -> b
$ StrengthenFail
e StrengthenFail -> [StrengthenFail] -> NonEmpty StrengthenFail
forall a. a -> [a] -> NonEmpty a
:| [])
          Success s
s   -> (Natural
n, S1 ms (Rec0 s) p
-> Validation (NonEmpty StrengthenFail) (S1 ms (Rec0 s) p)
forall e a. a -> Validation e a
Success (S1 ms (Rec0 s) p
 -> Validation (NonEmpty StrengthenFail) (S1 ms (Rec0 s) p))
-> S1 ms (Rec0 s) p
-> Validation (NonEmpty StrengthenFail) (S1 ms (Rec0 s) p)
forall a b. (a -> b) -> a -> b
$ Rec0 s p -> S1 ms (Rec0 s) p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Rec0 s p -> S1 ms (Rec0 s) p) -> Rec0 s p -> S1 ms (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)

-- | 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 -> *) -> k1 -> *) (f :: k1 -> *)
       (a :: k1).
Constructor c =>
t c f a -> String
forall {k} (c :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (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 -> *) -> k1 -> *) (f :: k1 -> *)
       (a :: k1).
Datatype d =>
t d f a -> String
forall {k} (d :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (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 -> *) -> k1 -> *) (f :: k1 -> *)
       (a :: k1).
Selector s =>
t s f a -> String
forall {k} (s :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
       (f :: k1 -> *) (a :: k1).
Selector s =>
t s f a -> String
selName @s Any s Any Any
forall a. HasCallStack => a
undefined