{- | '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 = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (w :: k -> Type) (s :: k -> Type) (p :: k).
GStrengthenD w s =>
w p -> Validation (NonEmpty StrengthenFail) (s p)
gstrengthenD forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (w :: k -> Type) (s :: k -> Type) (p :: k).
GStrengthenC w s =>
String
-> String -> w p -> Validation (NonEmpty StrengthenFail) (s p)
gstrengthenC (forall {k} (d :: k). Datatype d => String
datatypeName' @dw) (forall {k} (d :: k). Datatype d => String
datatypeName' @ds) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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
_ = 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 -> forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (w :: k -> Type) (s :: k -> Type) (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 -> forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (w :: k -> Type) (s :: k -> Type) (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 = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (w :: k -> Type) (s :: k -> Type) (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
conName' @cw) (forall {k} (c :: k). Constructor c => String
conName' @cs) Natural
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (f :: k -> Type) (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, 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'', forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall k (f :: k -> Type) (g :: k -> Type) (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') = forall {k} (w :: k -> Type) (s :: k -> Type) (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') = forall {k} (w :: k -> Type) (s :: k -> Type) (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'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, forall e a. a -> Validation e a
Success (forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (forall k i (c :: Meta) (f :: k -> Type) (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 forall a.
Strengthen a =>
Weak a -> Validation (NonEmpty StrengthenFail) a
strengthen w
w of
          Failure NonEmpty StrengthenFail
es ->
            let fw :: Maybe String
fw = forall {k} (s :: k). Selector s => Maybe String
selName'' @mw
                fs :: Maybe String
fs = forall {k} (s :: k). 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, forall e a. e -> Validation e a
Failure forall a b. (a -> b) -> a -> b
$ StrengthenFail
e forall a. a -> [a] -> NonEmpty a
:| [])
          Success s
s   -> (Natural
n, forall e a. a -> Validation e a
Success forall a b. (a -> b) -> a -> b
$ forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 forall a b. (a -> b) -> a -> b
$ 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 {k} (s :: k). Selector s => String
selName' @s of String
"" -> forall a. Maybe a
Nothing
                                String
s  -> 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 {k} (c :: k) k1 (t :: k -> (k1 -> Type) -> k1 -> Type)
       (f :: k1 -> Type) (a :: k1).
Constructor c =>
t c f a -> String
conName @c 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 {k} (d :: k) k1 (t :: k -> (k1 -> Type) -> k1 -> Type)
       (f :: k1 -> Type) (a :: k1).
Datatype d =>
t d f a -> String
datatypeName @d 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 {k} (s :: k) k1 (t :: k -> (k1 -> Type) -> k1 -> Type)
       (f :: k1 -> Type) (a :: k1).
Selector s =>
t s f a -> String
selName @s forall a. HasCallStack => a
undefined